set X = { { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } where i is Nat : i < len p } ;
A1: tree p c= {{}} \/ (union { { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } where i is Nat : i < len p } )
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in tree p or x in {{}} \/ (union { { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } where i is Nat : i < len p } ) )
assume A2: x in tree p ; :: thesis: x in {{}} \/ (union { { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } where i is Nat : i < len p } )
reconsider xx = x as set by TARSKI:1;
per cases ( x = {} or ex n being Nat ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) by A2, TREES_3:def 15;
suppose x = {} ; :: thesis: x in {{}} \/ (union { { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } where i is Nat : i < len p } )
then x in {{}} by TARSKI:def 1;
hence x in {{}} \/ (union { { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } where i is Nat : i < len p } ) by XBOOLE_0:def 3; :: thesis: verum
end;
suppose ex n being Nat ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ; :: thesis: x in {{}} \/ (union { { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } where i is Nat : i < len p } )
then consider n being Nat, q being FinSequence such that
A3: ( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ;
( 1 <= n + 1 & n + 1 <= len p ) by A3, NAT_1:11, NAT_1:13;
then n + 1 in dom p by FINSEQ_3:25;
then ( p . (n + 1) in rng p & rng p is constituted-Trees ) by FUNCT_1:def 3, TREES_3:def 9;
then reconsider t = p . (n + 1) as Tree ;
q is Element of t by A3;
then q in NAT * by FINSEQ_1:def 11;
then A4: x in { (<*n*> ^ w) where w is Element of NAT * : w in p . (n + 1) } by A3;
{ (<*n*> ^ w) where w is Element of NAT * : w in p . (n + 1) } in { { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } where i is Nat : i < len p } by A3;
then x in union { { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } where i is Nat : i < len p } by A4, TARSKI:def 4;
hence x in {{}} \/ (union { { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } where i is Nat : i < len p } ) by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
deffunc H2( object ) -> set = { (<*i*> ^ q) where q is Element of NAT * , i is Nat : ( p = i + 1 & q in p . (i + 1) ) } ;
consider f being Function such that
A5: ( dom f = dom p & ( for x being object st x in dom p holds
f . x = H2(x) ) ) from FUNCT_1:sch 3();
 A6: rng f = { { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } where i is Nat : i < len p }
proof
thus rng f c= { { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } where i is Nat : i < len p } :: according to XBOOLE_0:def 10 :: thesis: { { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } where i is Nat : i < len p } c= rng f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in { { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } where i is Nat : i < len p } )
reconsider xx = x as set by TARSKI:1;
assume x in rng f ; :: thesis: x in { { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } where i is Nat : i < len p }
then consider y being object such that
A7: ( y in dom f & x = f . y ) by FUNCT_1:def 3;
A8: x = H2(y) by A5, A7;
reconsider y = y as Element of NAT by A5, A7;
consider i being Nat such that
A9: y = 1 + i by A5, A7, FINSEQ_3:25, NAT_1:10;
y <= len p by A5, A7, FINSEQ_3:25;
then A10: i < len p by A9, NAT_1:13;
xx = { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) }
proof
thus xx c= { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } :: according to XBOOLE_0:def 10 :: thesis: { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } c= xx
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in xx or z in { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } )
assume z in xx ; :: thesis: z in { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) }
then consider q being Element of NAT * , j being Nat such that
A11: ( z = <*j*> ^ q & i + 1 = j + 1 & q in p . (j + 1) ) by A8, A9;
thus z in { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } by A11; :: thesis: verum
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } or z in xx )
assume z in { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } ; :: thesis: z in xx
then consider q being Element of NAT * such that
A12: ( z = <*i*> ^ q & q in p . (i + 1) ) ;
thus z in xx by A8, A9, A12; :: thesis: verum
end;
hence x in { { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } where i is Nat : i < len p } by A10; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } where i is Nat : i < len p } or x in rng f )
reconsider xx = x as set by TARSKI:1;
assume x in { { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } where i is Nat : i < len p } ; :: thesis: x in rng f
then consider i being Nat such that
A13: ( x = { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } & i < len p ) ;
A14: xx = H2(i + 1)
proof
thus xx c= H2(i + 1) :: according to XBOOLE_0:def 10 :: thesis: H2(i + 1) c= xx
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in xx or z in H2(i + 1) )
assume z in xx ; :: thesis: z in H2(i + 1)
then consider q being Element of NAT * such that
A15: ( z = <*i*> ^ q & q in p . (i + 1) ) by A13;
thus z in H2(i + 1) by A15; :: thesis: verum
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in H2(i + 1) or z in xx )
assume z in H2(i + 1) ; :: thesis: z in xx
then consider q being Element of NAT * , j being Nat such that
A16: ( z = <*j*> ^ q & i + 1 = j + 1 & q in p . (j + 1) ) ;
thus z in xx by A13, A16; :: thesis: verum
end;
A17: ( i + 1 >= 1 & i + 1 <= len p ) by A13, NAT_1:11, NAT_1:13;
then A18: i + 1 in dom f by A5, FINSEQ_3:25;
f . (i + 1) = x by A5, A14, A17, FINSEQ_3:25;
hence x in rng f by A18, FUNCT_1:def 3; :: thesis: verum
end;
now :: thesis: for x being set st x in { { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } where i is Nat : i < len p } holds
x is finite
let x be set ; :: thesis: ( x in { { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } where i is Nat : i < len p } implies x is finite )
assume x in { { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } where i is Nat : i < len p } ; :: thesis: x is finite
then consider i being Nat such that
A19: ( x = { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } & i < len p ) ;
( i + 1 >= 1 & i + 1 <= len p ) by A19, NAT_1:11, NAT_1:13;
then i + 1 in dom p by FINSEQ_3:25;
then ( p . (i + 1) in rng p & rng p is constituted-Trees ) by FUNCT_1:def 3, TREES_3:def 9;
then reconsider t = p . (i + 1) as finite Tree ;
deffunc H3( Element of t) -> FinSequence of NAT = <*i*> ^ p;
consider g being Function such that
A20: ( dom g = t & ( for x being Element of t holds g . x = H3(x) ) ) from FUNCT_1:sch 4();
A21: x c= rng g
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in x or z in rng g )
assume z in x ; :: thesis: z in rng g
then consider q being Element of NAT * such that
A22: ( z = <*i*> ^ q & q in p . (i + 1) ) by A19;
z = g . q by A20, A22;
hence z in rng g by A20, A22, FUNCT_1:def 3; :: thesis: verum
end;
rng g is finite by A20, FINSET_1:8;
hence x is finite by A21; :: thesis: verum
end;
then union { { (<*i*> ^ q) where q is Element of NAT * : q in p . (i + 1) } where i is Nat : i < len p } is finite by A6, A5, FINSET_1:7, FINSET_1:8;
hence tree p is finite by A1; :: thesis: verum