let x, y be set ; :: thesis: for p, q being FinSequence st x -flat_tree p = y -flat_tree q holds
( x = y & p = q )
let p, q be FinSequence; :: thesis: ( x -flat_tree p = y -flat_tree q implies ( x = y & p = q ) )
assume A1: x -flat_tree p = y -flat_tree q ; :: thesis: ( x = y & p = q )
A2: (x -flat_tree p) . {} = x by Def3;
thus x = y by A1, A2, Def3; :: thesis: p = q
A3: ( dom (x -flat_tree p) = elementary_tree (len p) & dom (y -flat_tree q) = elementary_tree (len q) ) by Def3;
A4: len p = len q by A1, A3, Th2;

A5: now

let i be Nat; :: thesis: ( i >= 1 & i <= len p implies p . i = q . i )
assume that
A6: i >= 1 and
A7: i <= len p ; :: thesis: p . i = q . i
consider n being Nat such that
A8: i = 1 + n by A6, NAT_1:10;
A9: ( n in NAT & n < len p ) by A7, A8, NAT_1:13, ORDINAL1:def 13;
A10: p . i = (x -flat_tree p) . <*n*> by A8, A9, Def3;
thus p . i = q . i by A1, A4, A8, A9, A10, Def3; :: thesis: verum

end;

thus p = q by A1, A3, A5, Th2, FINSEQ_1:18; :: thesis: verum