let Z1, Z2 be Tree; :: thesis: for p being FinSequence of NAT st p in Z1 holds
for v being Element of Z1 with-replacement (p,Z2)
for w being Element of Z2 st v = p ^ w holds
succ v, succ w are_equipotent
let p be FinSequence of NAT ; :: thesis: ( p in Z1 implies for v being Element of Z1 with-replacement (p,Z2)
for w being Element of Z2 st v = p ^ w holds
succ v, succ w are_equipotent )
assume A1: p in Z1 ; :: thesis: for v being Element of Z1 with-replacement (p,Z2)
for w being Element of Z2 st v = p ^ w holds
succ v, succ w are_equipotent
set T = Z1 with-replacement (p,Z2);
let t be Element of Z1 with-replacement (p,Z2); :: thesis: for w being Element of Z2 st t = p ^ w holds
succ t, succ w are_equipotent
let t2 be Element of Z2; :: thesis: ( t = p ^ t2 implies succ t, succ t2 are_equipotent )
assume A2: t = p ^ t2 ; :: thesis: succ t, succ t2 are_equipotent
then A3: p is_a_prefix_of t by TREES_1:1;
A4: for n being Element of NAT holds
( t ^ <*n*> in Z1 with-replacement (p,Z2) iff t2 ^ <*n*> in Z2 )

proof

let n be Element of NAT ; :: thesis: ( t ^ <*n*> in Z1 with-replacement (p,Z2) iff t2 ^ <*n*> in Z2 )
A5: p is_a_proper_prefix_of t ^ <*n*> by A3, TREES_1:8;
A6: t ^ <*n*> = p ^ (t2 ^ <*n*>) by A2, FINSEQ_1:32;
thus ( t ^ <*n*> in Z1 with-replacement (p,Z2) implies t2 ^ <*n*> in Z2 ) :: thesis: ( t2 ^ <*n*> in Z2 implies t ^ <*n*> in Z1 with-replacement (p,Z2) )

proof

assume t ^ <*n*> in Z1 with-replacement (p,Z2) ; :: thesis: t2 ^ <*n*> in Z2
then ex w being FinSequence of NAT st
( w in Z2 & t ^ <*n*> = p ^ w ) by A1, A5, TREES_1:def 9;
hence t2 ^ <*n*> in Z2 by A6, FINSEQ_1:33; :: thesis: verum

end;

assume t2 ^ <*n*> in Z2 ; :: thesis: t ^ <*n*> in Z1 with-replacement (p,Z2)
hence t ^ <*n*> in Z1 with-replacement (p,Z2) by A1, A6, TREES_1:def 9; :: thesis: verum

end;

defpred S₁[ set , set ] means for n being Element of NAT st $1 = t ^ <*n*> holds
$2 = t2 ^ <*n*>;
A7: for x being set st x in succ t holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in succ t implies ex y being set st S₁[x,y] )
assume x in succ t ; :: thesis: ex y being set st S₁[x,y]
then consider n being Element of NAT such that
A8: x = t ^ <*n*> and
t ^ <*n*> in Z1 with-replacement (p,Z2) ;
take t2 ^ <*n*> ; :: thesis: S₁[x,t2 ^ <*n*>]
let m be Element of NAT ; :: thesis: ( x = t ^ <*m*> implies t2 ^ <*n*> = t2 ^ <*m*> )
assume x = t ^ <*m*> ; :: thesis: t2 ^ <*n*> = t2 ^ <*m*>
hence t2 ^ <*n*> = t2 ^ <*m*> by A8, FINSEQ_1:33; :: thesis: verum

end;

consider f being Function such that
A9: ( dom f = succ t & ( for x being set st x in succ t holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A7);

now

let x be set ; :: thesis: ( ( x in rng f implies x in succ t2 ) & ( x in succ t2 implies x in rng f ) )
thus ( x in rng f implies x in succ t2 ) :: thesis: ( x in succ t2 implies x in rng f )

proof

assume x in rng f ; :: thesis: x in succ t2
then consider y being set such that
A10: y in dom f and
A11: x = f . y by FUNCT_1:def 3;
consider n being Element of NAT such that
A12: y = t ^ <*n*> and
A13: t ^ <*n*> in Z1 with-replacement (p,Z2) by A9, A10;
A14: x = t2 ^ <*n*> by A9, A10, A11, A12;
t2 ^ <*n*> in Z2 by A4, A13;
hence x in succ t2 by A14; :: thesis: verum

end;

assume x in succ t2 ; :: thesis: x in rng f
then consider n being Element of NAT such that
A15: x = t2 ^ <*n*> and
A16: t2 ^ <*n*> in Z2 ;
t ^ <*n*> in Z1 with-replacement (p,Z2) by A4, A16;
then A17: t ^ <*n*> in dom f by A9;
then f . (t ^ <*n*>) = x by A9, A15;
hence x in rng f by A17, FUNCT_1:def 3; :: thesis: verum

end;

then A18: rng f = succ t2 by TARSKI:1;
f is one-to-one

proof

let x1 be set ; :: according to FUNCT_1:def 4 :: thesis: for b₁ being set holds
( not x1 in proj1 f or not b₁ in proj1 f or not f . x1 = f . b₁ or x1 = b₁ )
let x2 be set ; :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A19: x1 in dom f and
A20: x2 in dom f and
A21: f . x1 = f . x2 ; :: thesis: x1 = x2
consider m being Element of NAT such that
A22: x1 = t ^ <*m*> and
t ^ <*m*> in Z1 with-replacement (p,Z2) by A9, A19;
consider k being Element of NAT such that
A23: x2 = t ^ <*k*> and
t ^ <*k*> in Z1 with-replacement (p,Z2) by A9, A20;
t2 ^ <*m*> = f . x1 by A9, A19, A22
.= t2 ^ <*k*> by A9, A20, A21, A23 ;
hence x1 = x2 by A22, A23, FINSEQ_1:33; :: thesis: verum

end;

hence succ t, succ t2 are_equipotent by A9, A18, WELLORD2:def 4; :: thesis: verum