defpred S₁[ set ] means for p being FinTree-yielding FinSequence st len p = p holds
tree p is finite Tree;
A1: S₁[ 0 ]

proof

let p be FinTree-yielding FinSequence; :: thesis: ( len p = 0 implies tree p is finite Tree )
assume len p = 0 ; :: thesis: tree p is finite Tree
then p = {} ;
hence tree p is finite Tree by Th52; :: thesis: verum

end;

A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: for p being FinTree-yielding FinSequence st len p = n holds
tree p is finite Tree ; :: thesis: S₁[n + 1]
let p be FinTree-yielding FinSequence; :: thesis: ( len p = n + 1 implies tree p is finite Tree )
assume A4: len p = n + 1 ; :: thesis: tree p is finite Tree
p <> {} by A4;
then consider q being FinSequence, x being object such that
A5: p = q ^ <*x*> by FINSEQ_1:46;
reconsider q = q as FinTree-yielding FinSequence by A5, Th26;
len <*x*> = 1 by FINSEQ_1:40;
then A6: len p = (len q) + 1 by A5, FINSEQ_1:22;
then tree q is finite by A3, A4;
then reconsider W = (tree q) \/ (elementary_tree (n + 1)) as finite Tree ;
<*x*> is FinTree-yielding by A5, Th26;
then reconsider x = x as finite Tree by Th29;
n < n + 1 by NAT_1:13;
then <*n*> in elementary_tree (n + 1) by TREES_1:28;
then reconsider r = <*n*> as Element of W by XBOOLE_0:def 3;
tree p = W with-replacement (r,x) by A4, A5, A6, Th55;
hence tree p is finite Tree ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
then ( len p = len p implies tree p is finite ) ;
hence tree p is finite ; :: thesis: verum