let Z be Tree; :: thesis: for o being Element of Z st o <> Root Z holds
( Z | o,{ (o ^ s') where s' is Element of NAT * : o ^ s' in Z } are_equipotent & not Root Z in { (o ^ w') where w' is Element of NAT * : o ^ w' in Z } )
let o be Element of Z; :: thesis: ( o <> Root Z implies ( Z | o,{ (o ^ s') where s' is Element of NAT * : o ^ s' in Z } are_equipotent & not Root Z in { (o ^ w') where w' is Element of NAT * : o ^ w' in Z } ) )
assume A1: o <> Root Z ; :: thesis: ( Z | o,{ (o ^ s') where s' is Element of NAT * : o ^ s' in Z } are_equipotent & not Root Z in { (o ^ w') where w' is Element of NAT * : o ^ w' in Z } )
set A = { (o ^ s') where s' is Element of NAT * : o ^ s' in Z } ;
thus Z | o,{ (o ^ s') where s' is Element of NAT * : o ^ s' in Z } are_equipotent :: thesis: not Root Z in { (o ^ w') where w' is Element of NAT * : o ^ w' in Z }

proof

defpred S₁[ set , set ] means for s being FinSequence of NAT st $1 = s holds
$2 = o ^ s;
A4: for x being set st x in Z | o holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in Z | o implies ex y being set st S₁[x,y] )
assume x in Z | o ; :: thesis: ex y being set st S₁[x,y]
then reconsider s = x as FinSequence of NAT by TREES_1:44;
take o ^ s ; :: thesis: S₁[x,o ^ s]
let w be FinSequence of NAT ; :: thesis: ( x = w implies o ^ s = o ^ w )
assume x = w ; :: thesis: o ^ s = o ^ w
hence o ^ s = o ^ w ; :: thesis: verum

end;

ex f being Function st
( dom f = Z | o & ( for x being set st x in Z | o holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A4);
then consider f being Function such that
A5: dom f = Z | o and
A6: for x being set st x in Z | o holds
for s being FinSequence of NAT st x = s holds
f . x = o ^ s ;
A7: rng f = { (o ^ s') where s' is Element of NAT * : o ^ s' in Z }

proof

now

let x be set ; :: thesis: ( ( x in rng f implies x in { (o ^ s') where s' is Element of NAT * : o ^ s' in Z } ) & ( x in { (o ^ s') where s' is Element of NAT * : o ^ s' in Z } implies x in rng f ) )
thus ( x in rng f implies x in { (o ^ s') where s' is Element of NAT * : o ^ s' in Z } ) :: thesis: ( x in { (o ^ s') where s' is Element of NAT * : o ^ s' in Z } implies x in rng f )

proof

assume x in rng f ; :: thesis: x in { (o ^ s') where s' is Element of NAT * : o ^ s' in Z }
then consider x1 being set such that
A8: ( x1 in dom f & x = f . x1 ) by FUNCT_1:def 5;
reconsider x1 = x1 as FinSequence of NAT by A5, A8, TREES_1:44;
reconsider x1 = x1 as Element of NAT * by FINSEQ_1:def 11;
A9: o ^ x1 in Z by A5, A8, TREES_1:def 9;
( x = o ^ x1 & x1 is Element of NAT * ) by A5, A6, A8;
hence x in { (o ^ s') where s' is Element of NAT * : o ^ s' in Z } by A9; :: thesis: verum

end;

assume x in { (o ^ s') where s' is Element of NAT * : o ^ s' in Z } ; :: thesis: x in rng f
then consider v' being Element of NAT * such that
A10: ( x = o ^ v' & o ^ v' in Z ) ;
A11: v' in Z | o by A10, TREES_1:def 9;
A12: v' in dom f by A5, A10, TREES_1:def 9;
x = f . v' by A6, A10, A11;
hence x in rng f by A12, FUNCT_1:def 5; :: thesis: verum

end;

hence rng f = { (o ^ s') where s' is Element of NAT * : o ^ s' in Z } by TARSKI:2; :: thesis: verum

end;

f is one-to-one

proof

now

let x1, x2 be set ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume A13: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then reconsider s1 = x1, s2 = x2 as FinSequence of NAT by A5, TREES_1:44;
o ^ s1 = f . x2 by A5, A6, A13
.= o ^ s2 by A5, A6, A13 ;
hence x1 = x2 by FINSEQ_1:46; :: thesis: verum

end;

hence f is one-to-one by FUNCT_1:def 8; :: thesis: verum

end;

hence Z | o,{ (o ^ s') where s' is Element of NAT * : o ^ s' in Z } are_equipotent by A5, A7, WELLORD2:def 4; :: thesis: verum

end;

assume Root Z in { (o ^ w') where w' is Element of NAT * : o ^ w' in Z } ; :: thesis: contradiction
then consider v' being Element of NAT * such that
A14: ( Root Z = o ^ v' & o ^ v' in Z ) ;
thus contradiction by A1, A14; :: thesis: verum