let p, q be Tree-yielding FinSequence; :: thesis: ( tree p = tree q implies p = q )
assume A1: tree p = tree q ; :: thesis: p = q
A2: ( (tree p) -level 1 = { <*n*> where n is Element of NAT : n < len p } & (tree q) -level 1 = { <*k*> where k is Element of NAT : k < len q } & ( for n being Element of NAT st n < len p holds
(tree p) | <*n*> = p . (n + 1) ) & ( for n being Element of NAT st n < len q holds
(tree q) | <*n*> = q . (n + 1) ) ) by Th52;

now

let n1, n2 be Element of NAT ; :: thesis: ( { <*i*> where i is Element of NAT : i < n1 } = { <*k*> where k is Element of NAT : k < n2 } implies not n1 < n2 )
assume ( { <*i*> where i is Element of NAT : i < n1 } = { <*k*> where k is Element of NAT : k < n2 } & n1 < n2 ) ; :: thesis: contradiction
then <*n1*> in { <*i*> where i is Element of NAT : i < n1 } ;
then consider i being Element of NAT such that
A3: ( <*n1*> = <*i*> & i < n1 ) ;
( <*n1*> . 1 = n1 & <*i*> . 1 = i ) by FINSEQ_1:57;
hence contradiction by A3; :: thesis: verum

end;

then ( not len p < len q & not len p > len q ) by A1, A2;
then A4: len p = len q by XXREAL_0:1;

now

let i be Nat; :: thesis: ( i >= 1 & i <= len p implies p . i = q . i )
assume A5: ( i >= 1 & i <= len p ) ; :: thesis: p . i = q . i
then consider k being Nat such that
A6: i = 1 + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
k < len p by A5, A6, NAT_1:13;
then ( p . i = (tree p) | <*k*> & q . i = (tree q) | <*k*> ) by A4, A6, Th52;
hence p . i = q . i by A1; :: thesis: verum

end;

hence p = q by A4, FINSEQ_1:18; :: thesis: verum