let T be finite-branching Tree; :: thesis: for n being Nat holds T -level n is finite
defpred S₁[ Nat] means T -level $1 is finite ;
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: T -level n is finite ; :: thesis: S₁[n + 1]
set X = { (succ w) where w is Element of T : len w = n } ;
A3: { (succ w) where w is Element of T : len w = n } is finite

proof

defpred S₂[ object , object ] means ex w being Element of T st
( $1 = w & $2 = succ w );
A4: for x being object st x in T -level n holds
ex y being object st S₂[x,y]

proof

let x be object ; :: thesis: ( x in T -level n implies ex y being object st S₂[x,y] )
assume x in T -level n ; :: thesis: ex y being object st S₂[x,y]
then consider w being Element of T such that
A5: w = x ;
consider y being set such that
A6: y = succ w ;
take y ; :: thesis: S₂[x,y]
take w ; :: thesis: ( x = w & y = succ w )
thus ( x = w & y = succ w ) by A5, A6; :: thesis: verum

end;

consider f being Function such that
A7: ( dom f = T -level n & ( for x being object st x in T -level n holds
S₂[x,f . x] ) ) from CLASSES1:sch 1(A4);
A8: { (succ w) where w is Element of T : len w = n } c= rng f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (succ w) where w is Element of T : len w = n } or x in rng f )
assume x in { (succ w) where w is Element of T : len w = n } ; :: thesis: x in rng f
then consider w being Element of T such that
A9: x = succ w and
A10: len w = n ;
A11: w in T -level n by A10;
then ex w9 being Element of T st
( w = w9 & f . w = succ w9 ) by A7;
hence x in rng f by A7, A9, A11, FUNCT_1:def 3; :: thesis: verum

end;

card (rng f) c= card (dom f) by CARD_1:12;
then rng f is finite by A2, A7;
hence { (succ w) where w is Element of T : len w = n } is finite by A8; :: thesis: verum

end;

A12: for Y being set st Y in { (succ w) where w is Element of T : len w = n } holds
Y is finite

proof

let Y be set ; :: thesis: ( Y in { (succ w) where w is Element of T : len w = n } implies Y is finite )
assume Y in { (succ w) where w is Element of T : len w = n } ; :: thesis: Y is finite
then ex w being Element of T st
( Y = succ w & len w = n ) ;
hence Y is finite ; :: thesis: verum

end;

T -level (n + 1) = union { (succ w) where w is Element of T : len w = n } by Th45;
hence S₁[n + 1] by A3, A12, FINSET_1:7; :: thesis: verum

end;

A13: S₁[ 0 ] by Th44;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A13, A1); :: thesis: verum