let x, y be set ; :: thesis: for p, q being DTree-yielding FinSequence st x -tree p = y -tree q holds
( x = y & p = q )
let p, q be DTree-yielding FinSequence; :: thesis: ( x -tree p = y -tree q implies ( x = y & p = q ) )
assume A1: x -tree p = y -tree q ; :: thesis: ( x = y & p = q )
A2: (x -tree p) . {} = x by Def4;
thus x = y by A1, A2, Def4; :: thesis: p = q
A3: ( dom (x -tree p) = tree (doms p) & dom (y -tree q) = tree (doms q) ) by Th10;
A4: doms p = doms q by A1, A3, TREES_3:53;
A5: ( dom p = dom (doms p) & dom (doms q) = dom q ) by TREES_3:39;
A6: len p = len q by A4, A5, FINSEQ_3:31;

A7: now

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

end;

thus p = q by A6, A7, FINSEQ_1:18; :: thesis: verum