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

proof

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

proof

let x be object ; :: thesis: ( x in Z | o implies ex y being object st S₁[x,y] )
assume x in Z | o ; :: thesis: ex y being object st S₁[x,y]
then reconsider s = x as FinSequence of NAT by TREES_1:19;
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 object st x in Z | o holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A2);
then consider f being Function such that
A3: dom f = Z | o and
A4: for x being object st x in Z | o holds
for s being FinSequence of NAT st x = s holds
f . x = o ^ s ;

now :: thesis: for x being object holds
( ( x in rng f implies x in { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } ) & ( x in { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } implies x in rng f ) )

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

proof

assume x in rng f ; :: thesis: x in { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z }
then consider x1 being object such that
A5: x1 in dom f and
A6: x = f . x1 by FUNCT_1:def 3;
reconsider x1 = x1 as FinSequence of NAT by A3, A5, TREES_1:19;
reconsider x1 = x1 as Element of NAT * by FINSEQ_1:def 11;
( o ^ x1 in Z & x = o ^ x1 ) by A3, A4, A5, A6, TREES_1:def 6;
hence x in { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } ; :: thesis: verum

end;

assume x in { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } ; :: thesis: x in rng f
then consider v9 being Element of NAT * such that
A7: x = o ^ v9 and
A8: o ^ v9 in Z ;
v9 in Z | o by A8, TREES_1:def 6;
then A9: x = f . v9 by A4, A7;
v9 in dom f by A3, A8, TREES_1:def 6;
hence x in rng f by A9, FUNCT_1:def 3; :: thesis: verum

end;

then A10: rng f = { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } by TARSKI:2;

now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A11: x1 in dom f and
A12: x2 in dom f and
A13: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider s1 = x1, s2 = x2 as FinSequence of NAT by A3, A11, A12, TREES_1:19;
o ^ s1 = f . x2 by A3, A4, A11, A13
.= o ^ s2 by A3, A4, A12 ;
hence x1 = x2 by FINSEQ_1:33; :: thesis: verum

end;

then f is one-to-one by FUNCT_1:def 4;
hence Z | o, { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } are_equipotent by A3, A10, WELLORD2:def 4; :: thesis: verum

end;

assume Root Z in { (o ^ w9) where w9 is Element of NAT * : o ^ w9 in Z } ; :: thesis: contradiction
then ex v9 being Element of NAT * st
( Root Z = o ^ v9 & o ^ v9 in Z ) ;
hence contradiction by A1; :: thesis: verum