let x1, x2 be FinSequence; :: thesis: ( dom x1 = dom p & ( for i being Element of NAT st i in dom p holds
ex T being DecoratedTree st
( T = p . i & x1 . i = T . {} ) ) & dom x2 = dom p & ( for i being Element of NAT st i in dom p holds
ex T being DecoratedTree st
( T = p . i & x2 . i = T . {} ) ) implies x1 = x2 )
assume that
A5: dom x1 = dom p and
A6: for i being Element of NAT st i in dom p holds
S₁[i,x1 . i] and
A7: dom x2 = dom p and
A8: for i being Element of NAT st i in dom p holds
S₁[i,x2 . i] ; :: thesis: x1 = x2

now :: thesis: for k being Nat st k in dom p holds
x1 . k = x2 . k

let k be Nat; :: thesis: ( k in dom p implies x1 . k = x2 . k )
assume A9: k in dom p ; :: thesis: x1 . k = x2 . k
then A10: S₁[k,x1 . k] by A6;
S₁[k,x2 . k] by A8, A9;
hence x1 . k = x2 . k by A10; :: thesis: verum

end;

hence x1 = x2 by A5, A7, FINSEQ_1:13; :: thesis: verum