let Z1 be Tree; :: thesis: for p being FinSequence of NAT st p in Z1 holds
for v being Element of Z1
for w being Element of Z1 | p 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
for w being Element of Z1 | p st v = p ^ w holds
succ v, succ w are_equipotent )
assume A1: p in Z1 ; :: thesis: for v being Element of Z1
for w being Element of Z1 | p st v = p ^ w holds
succ v, succ w are_equipotent
set T = Z1 | p;
let t be Element of Z1; :: thesis: for w being Element of Z1 | p st t = p ^ w holds
succ t, succ w are_equipotent
let t2 be Element of Z1 | p; :: thesis: ( t = p ^ t2 implies succ t, succ t2 are_equipotent )
assume A2: t = p ^ t2 ; :: thesis: succ t, succ t2 are_equipotent
A3: for n being Element of NAT holds
( t ^ <*n*> in Z1 iff t2 ^ <*n*> in Z1 | p )

proof

let n be Element of NAT ; :: thesis: ( t ^ <*n*> in Z1 iff t2 ^ <*n*> in Z1 | p )
A4: t ^ <*n*> = p ^ (t2 ^ <*n*>) by A2, FINSEQ_1:45;
hence ( t ^ <*n*> in Z1 implies t2 ^ <*n*> in Z1 | p ) by A1, TREES_1:def 9; :: thesis: ( t2 ^ <*n*> in Z1 | p implies t ^ <*n*> in Z1 )
assume t2 ^ <*n*> in Z1 | p ; :: thesis: t ^ <*n*> in Z1
hence t ^ <*n*> in Z1 by A1, A4, 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*>;
A8: 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 x in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in Z1 } by TREES_2:def 5;
then consider n being Element of NAT such that
A9: ( x = t ^ <*n*> & t ^ <*n*> in Z1 ) ;
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 A9, FINSEQ_1:46; :: thesis: verum

end;

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

proof

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
A12: ( y in dom f & x = f . y ) by FUNCT_1:def 5;
y in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in Z1 } by A10, A12, TREES_2:def 5;
then consider n being Element of NAT such that
A13: ( y = t ^ <*n*> & t ^ <*n*> in Z1 ) ;
A14: x = t2 ^ <*n*> by A10, A12, A13;
t2 ^ <*n*> in Z1 | p by A3, A13;
then x in { (t2 ^ <*m*>) where m is Element of NAT : t2 ^ <*m*> in Z1 | p } by A14;
hence x in succ t2 by TREES_2:def 5; :: thesis: verum

end;

assume x in succ t2 ; :: thesis: x in rng f
then x in { (t2 ^ <*n*>) where n is Element of NAT : t2 ^ <*n*> in Z1 | p } by TREES_2:def 5;
then consider n being Element of NAT such that
A15: ( x = t2 ^ <*n*> & t2 ^ <*n*> in Z1 | p ) ;
t ^ <*n*> in Z1 by A3, A15;
then t ^ <*n*> in { (t ^ <*m*>) where m is Element of NAT : t ^ <*m*> in Z1 } ;
then A16: t ^ <*n*> in dom f by A10, TREES_2:def 5;
then f . (t ^ <*n*>) = x by A10, A15;
hence x in rng f by A16, FUNCT_1:def 5; :: thesis: verum

end;

hence rng f = succ t2 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 A17: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then x1 in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in Z1 } by A10, TREES_2:def 5;
then consider m being Element of NAT such that
A18: ( x1 = t ^ <*m*> & t ^ <*m*> in Z1 ) ;
x2 in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in Z1 } by A10, A17, TREES_2:def 5;
then consider k being Element of NAT such that
A19: ( x2 = t ^ <*k*> & t ^ <*k*> in Z1 ) ;
t2 ^ <*m*> = f . x1 by A10, A17, A18
.= t2 ^ <*k*> by A10, A17, A19 ;
hence x1 = x2 by A18, A19, FINSEQ_1:46; :: thesis: verum

end;

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

end;

hence succ t, succ t2 are_equipotent by A10, A11, WELLORD2:def 4; :: thesis: verum