let p, q be Tree-yielding FinSequence; ( tree p = tree q implies p = q )
assume A1:
tree p = tree q
; 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;
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;
hence
p = q
by A6, A7, FINSEQ_1:14, XXREAL_0:1; verum