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 Nat : n < len p } by Th49;
A3: (tree q) -level 1 = { <*k*> where k is Nat : k < len q } by Th49;

A4: now :: thesis: for n1, n2 being Element of NAT st { <*i*> where i is Nat : i < n1 } = { <*k*> where k is Nat : k < n2 } holds
not n1 < n2

let n1, n2 be Element of NAT ; :: thesis: ( { <*i*> where i is Nat : i < n1 } = { <*k*> where k is Nat : k < n2 } implies not n1 < n2 )
assume ( { <*i*> where i is Nat : i < n1 } = { <*k*> where k is Nat : k < n2 } & n1 < n2 ) ; :: thesis: contradiction
then <*n1*> in { <*i*> where i is Nat : i < n1 } ;
then A5: ex i being Nat st
( <*n1*> = <*i*> & i < n1 ) ;
<*n1*> . 1 = n1 ;
hence contradiction by A5, FINSEQ_1:40; :: thesis: verum

end;

then A6: not len p < len q by A1, A2, A3;
A7: not len p > len q by A1, A2, A3, A4;
then A8: len p = len q by A6, XXREAL_0:1;

now :: thesis: for i being Nat st i >= 1 & i <= len p holds
p . i = q . i

let i be Nat; :: thesis: ( i >= 1 & i <= len p implies p . i = q . i )
assume that
A9: i >= 1 and
A10: i <= len p ; :: thesis: p . i = q . i
consider k being Nat such that
A11: i = 1 + k by A9, NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
A12: k < len p by A10, A11, NAT_1:13;
then p . i = (tree p) | <*k*> by A11, Th49;
hence p . i = q . i by A1, A8, A11, A12, Th49; :: thesis: verum

end;

hence p = q by A6, A7, FINSEQ_1:14, XXREAL_0:1; :: thesis: verum