for p1, p2 being FinSequence of K st len p1 = n & ( for i, j being Nat st i in dom p1 & j = p . i holds
p1 . i = M * i,j ) & len p2 = n & ( for i, j being Nat st i in dom p2 & j = p . i holds
p2 . i = M * i,j ) holds
p1 = p2

proof

let p1, p2 be FinSequence of K; :: thesis: ( len p1 = n & ( for i, j being Nat st i in dom p1 & j = p . i holds
p1 . i = M * i,j ) & len p2 = n & ( for i, j being Nat st i in dom p2 & j = p . i holds
p2 . i = M * i,j ) implies p1 = p2 )
assume that
A4: len p1 = n and
A5: for i, j being Nat st i in dom p1 & j = p . i holds
p1 . i = M * i,j and
A6: len p2 = n and
A7: for i, j being Nat st i in dom p2 & j = p . i holds
p2 . i = M * i,j ; :: thesis: p1 = p2
A8: dom p2 = Seg n by A6, FINSEQ_1:def 3;
A9: dom p1 = Seg n by A4, FINSEQ_1:def 3;
for i being Nat st i in Seg n holds
p1 . i = p2 . i

proof

reconsider p = p as Function of (Seg n),(Seg n) by MATRIX_2:def 11;
let i be Nat; :: thesis: ( i in Seg n implies p1 . i = p2 . i )
assume A10: i in Seg n ; :: thesis: p1 . i = p2 . i
then p . i in Seg n by FUNCT_2:7;
then reconsider j = p . i as Element of NAT ;
p1 . i = M * i,j by A5, A9, A10;
hence p1 . i = p2 . i by A7, A8, A10; :: thesis: verum

end;

hence p1 = p2 by A9, A8, FINSEQ_1:17; :: thesis: verum

end;

hence for b₁, b₂ being FinSequence of K st len b₁ = n & ( for i, j being Nat st i in dom b₁ & j = p . i holds
b₁ . i = M * i,j ) & len b₂ = n & ( for i, j being Nat st i in dom b₂ & j = p . i holds
b₂ . i = M * i,j ) holds
b₁ = b₂ ; :: thesis: verum