let p1, p2 be FinSequence of D; :: thesis: ( len p1 = width M & ( for j being Nat st j in Seg (width M) holds
p1 . j = M * i,j ) & len p2 = width M & ( for j being Nat st j in Seg (width M) holds
p2 . j = M * i,j ) implies p1 = p2 )
assume that
A4: len p1 = width M and
A5: for j being Nat st j in Seg (width M) holds
p1 . j = M * i,j and
A6: len p2 = width M and
A7: for j being Nat st j in Seg (width M) holds
p2 . j = M * i,j ; :: thesis: p1 = p2
X: dom p1 = Seg (width M) by A4, 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 ( p1 . j = M * i,j & p2 . j = M * i,j ) by A5, A7, X;
hence p1 . j = p2 . j ; :: thesis: verum

end;

hence p1 = p2 by A4, A6, FINSEQ_2:10; :: thesis: verum