let p1, p2 be FinSequence of D; :: thesis: ( len p1 = len M & ( for j being Nat st j in dom M holds
p1 . j = M * (j,i) ) & len p2 = len M & ( for j being Nat st j in dom M holds
p2 . j = M * (j,i) ) implies p1 = p2 )
assume that
A12: len p1 = len M and
A13: for j being Nat st j in dom M holds
p1 . j = M * (j,i) and
A14: len p2 = len M and
A15: for j being Nat st j in dom M holds
p2 . j = M * (j,i) ; :: thesis: p1 = p2
A16: dom p1 = Seg (len M) by A12, FINSEQ_1:def 3;
for j being Nat st j in dom p1 holds
p1 . j = p2 . j

proof

let j be Nat; :: thesis: ( j in dom p1 implies p1 . j = p2 . j )
assume j in dom p1 ; :: thesis: p1 . j = p2 . j
then A17: j in dom M by A16, FINSEQ_1:def 3;
then p1 . j = M * (j,i) by A13;
hence p1 . j = p2 . j by A15, A17; :: thesis: verum

end;

hence p1 = p2 by A12, A14, FINSEQ_2:9; :: thesis: verum