let t be Tree; :: thesis:
assume t is finite ; :: thesis:
then reconsider s = t as finite Tree ;
take n = (card s) + 1; :: according to TREES_2:def 2 :: thesis:
let x be Element of t; :: thesis:
deffunc H₁( Nat) -> set = x ^ <*(c₁ - 1)*>;
consider f being FinSequence such that
A1: ( len f = n & ( for i being Nat st i in dom f holds
f . i = H₁(i) ) ) from FINSEQ_1:sch 2();
A2: dom f = Seg n by A1, FINSEQ_1:def 3;
assume A3: x ^ <*n*> in t ; :: thesis:
A4: rng f c= succ x

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng f ; :: thesis:
then consider i being object such that
A5: i in dom f and
A6: y = f . i by FUNCT_1:def 3;
reconsider i = i as Nat by A5;
i >= 1 by A2, A5, FINSEQ_1:1;
then consider j being Nat such that
A7: i = 1 + j by NAT_1:10;
reconsider j = j as Nat ;
A8: j <= i by A7, NAT_1:11;
i <= n by A2, A5, FINSEQ_1:1;
then j <= n by A8, XXREAL_0:2;
then A9: x ^ <*j*> in t by A3, TREES_1:def 3;
i - 1 = j by A7;
then y = x ^ <*j*> by A1, A5, A6;
hence y in succ x by A9; :: thesis:

end;

let z, y be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A11: ( z in dom f & y in dom f ) and
A12: f . z = f . y ; :: thesis:
reconsider i1 = z, i2 = y as Nat by A11;
( f . z = x ^ <*(i1 - 1)*> & f . y = x ^ <*(i2 - 1)*> ) by A1, A11;
then <*(i1 - 1)*> = <*(i2 - 1)*> by A12, FINSEQ_1:33;
then i1 - 1 = <*(i2 - 1)*> . 1 by FINSEQ_1:40
.= i2 - 1 by FINSEQ_1:40 ;
hence z = y ; :: thesis:

end;