Finite sets are defined as sets that can be bijectively mapped to [n]={1,2,...n}. Prove that a subset T of a finite set S is finite. That's the stated problem.
It is not clear to me what can be taken as given axioms.
The resolution is clearly to show the existence of a bijection from a subset of [n] to [m] where m<n.
It's trivial to describe an algorithm that does this: start with the smallest element and map it to 1. Proceed through S, mapping each element to an element of [m]. For example if T ={2,5,6...} map it to {1,2,3...}. For the k+1 th element of S, map it to the successor of the image of the k-th element of S. (By successor, I mean add one)
This sounds like induction.
Question: is it permissible to use this description of an algorithm and call it a proof?
First you should try to prove the particular case "if $a \in X$, $X$ is finite then $X \setminus \{a\}$ is finite". This follows from the following lemma which has a simple proof
"If $f:X \to Y$ is a bijection, $x \in X$, $y \in Y$ then there is a bijection $g:X \to Y$ such that $g(x)=y$."
Then let $f:\{1, \cdots, n\} \to X$ be a bijection and suppose wlg that $f(n)=a$. Hence if $n=1$, $X \setminus \{a\}=\emptyset$ and if $n >1$, the restriction $f |_{\{1, \cdots, n-1\}}:\{1, \cdots, n-1\} \to X \setminus \{a\}$ is a bijection.
For the general case suppose $X$ is finite and let $S \subseteq X$. Take a bijection $f:\{1, \cdots, n\} \to X$ and let's prove the result by induction. For $n=1$, $S=X$ or $S = \emptyset$ and the result follows. Now the induction hypothesis is "If $X$ is finite, $f:\{1, \cdots, n\} \to X$ is a bijection and $S \subseteq X$ then $S$ is finite". Let $f:\{1, \cdots, n+1\} \to X$ be a bijection. If $S=X$ there is nothing to prove so suppose $S \neq X$. Choose $a \in X$ such that $x \notin S$. Hence $S \subseteq X \setminus \{a\}$. From the particular case there is a bijection between $\{1, \cdots, n\}$ and $X \setminus \{a\}$. Then $S$ is finite by the induction hypothesis.