let x, y be object ; :: 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 )

(x -tree p) . {} = x by Def4;

hence x = y by A1, Def4; :: thesis: p = q

( dom (x -tree p) = tree (doms p) & dom (y -tree q) = tree (doms q) ) by Th10;

then A2: doms p = doms q by A1, TREES_3:50;

( dom p = dom (doms p) & dom (doms q) = dom q ) by TREES_3:37;

then A3: len p = len q by A2, FINSEQ_3:29;

( 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 )

(x -tree p) . {} = x by Def4;

hence x = y by A1, Def4; :: thesis: p = q

( dom (x -tree p) = tree (doms p) & dom (y -tree q) = tree (doms q) ) by Th10;

then A2: doms p = doms q by A1, TREES_3:50;

( dom p = dom (doms p) & dom (doms q) = dom q ) by TREES_3:37;

then A3: len p = len q by A2, FINSEQ_3:29;

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

p . i = q . i

hence
p = q
by A3; :: thesis: verump . i = q . i

let i be Nat; :: thesis: ( i >= 1 & i <= len p implies p . i = q . i )

assume that

A4: i >= 1 and

A5: i <= len p ; :: thesis: p . i = q . i

consider n being Nat such that

A6: i = 1 + n by A4, NAT_1:10;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

A7: n < len p by A5, A6, NAT_1:13;

then p . i = (x -tree p) | <*n*> by A6, Def4;

hence p . i = q . i by A1, A3, A6, A7, Def4; :: thesis: verum

end;assume that

A4: i >= 1 and

A5: i <= len p ; :: thesis: p . i = q . i

consider n being Nat such that

A6: i = 1 + n by A4, NAT_1:10;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

A7: n < len p by A5, A6, NAT_1:13;

then p . i = (x -tree p) | <*n*> by A6, Def4;

hence p . i = q . i by A1, A3, A6, A7, Def4; :: thesis: verum