let Z1 be Tree; :: thesis:
let p be FinSequence of NAT ; :: thesis:
assume A1: p in Z1 ; :: thesis:
set T = Z1 | p;
let t be Element of Z1; :: thesis:
let t2 be Element of Z1 | p; :: thesis:
assume A2: t = p ^ t2 ; :: thesis:
A3: for n being Nat holds
( t ^ <*n*> in Z1 iff t2 ^ <*n*> in Z1 | p )

end;

defpred S₁[ object , object ] means for n being Nat st $1 = t ^ <*n*> holds
$2 = t2 ^ <*n*>;
A5: for x being object st x in succ t holds
ex y being object st S₁[x,y]

let x be object ; :: thesis:
assume x in succ t ; :: thesis:
then x in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in Z1 } by TREES_2:def 5;
then consider n being Nat such that
A6: x = t ^ <*n*> and
t ^ <*n*> in Z1 ;
take t2 ^ <*n*> ; :: thesis:
let m be Nat; :: thesis:
assume x = t ^ <*m*> ; :: thesis:
hence t2 ^ <*n*> = t2 ^ <*m*> by A6, FINSEQ_1:33; :: thesis:

end;

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

assume x in rng f ; :: thesis:
then consider y being object such that
A8: y in dom f and
A9: x = f . y by FUNCT_1:def 3;
y in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in Z1 } by A7, A8, TREES_2:def 5;
then consider n being Nat such that
A10: y = t ^ <*n*> and
A11: t ^ <*n*> in Z1 ;
A12: t2 ^ <*n*> in Z1 | p by A3, A11;
x = t2 ^ <*n*> by A7, A8, A9, A10;
then x in { (t2 ^ <*m*>) where m is Nat : t2 ^ <*m*> in Z1 | p } by A12;
hence x in succ t2 by TREES_2:def 5; :: thesis:

end;

assume x in succ t2 ; :: thesis:
then x in { (t2 ^ <*n*>) where n is Nat : t2 ^ <*n*> in Z1 | p } by TREES_2:def 5;
then consider n being Nat such that
A13: x = t2 ^ <*n*> and
A14: t2 ^ <*n*> in Z1 | p ;
t ^ <*n*> in Z1 by A3, A14;
then t ^ <*n*> in { (t ^ <*m*>) where m is Nat : t ^ <*m*> in Z1 } ;
then A15: t ^ <*n*> in dom f by A7, TREES_2:def 5;
then f . (t ^ <*n*>) = x by A7, A13;
hence x in rng f by A15, FUNCT_1:def 3; :: thesis:

end;

let x1, x2 be object ; :: thesis:
assume that
A17: x1 in dom f and
A18: x2 in dom f and
A19: f . x1 = f . x2 ; :: thesis:
x2 in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in Z1 } by A7, A18, TREES_2:def 5;
then consider k being Nat such that
A20: x2 = t ^ <*k*> and
t ^ <*k*> in Z1 ;
x1 in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in Z1 } by A7, A17, TREES_2:def 5;
then consider m being Nat such that
A21: x1 = t ^ <*m*> and
t ^ <*m*> in Z1 ;
t2 ^ <*m*> = f . x1 by A7, A17, A21
.= t2 ^ <*k*> by A7, A18, A19, A20 ;
hence x1 = x2 by A21, A20, FINSEQ_1:33; :: thesis:

end;