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 Th55; :: thesis: verum

end;

A2: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of 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 set such that
A5: p = q ^ <*x*> by FINSEQ_1:63;
reconsider q = q as FinTree-yielding FinSequence by A5, Th28;
len <*x*> = 1 by FINSEQ_1:57;
then A6: len p = (len q) + 1 by A5, FINSEQ_1:35;
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, Th28;
then reconsider x = x as finite Tree by Th31;
n < n + 1 by NAT_1:13;
then <*n*> in elementary_tree (n + 1) by TREES_1:55;
then reconsider r = <*n*> as Element of W by XBOOLE_0:def 3;
tree p = W with-replacement r,x by A4, A5, A6, Th58;
hence tree p is finite Tree ; :: thesis: verum

end;

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