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
A6: len p1 = n and
A7: for i, j being Nat st i in dom p1 & j = p . i holds
p1 . i = M * i,j and
A8: len p2 = n and
A9: for i, j being Nat st i in dom p2 & j = p . i holds
p2 . i = M * i,j ; :: thesis: p1 = p2
A10: ( dom p1 = Seg n & dom p2 = Seg n ) by A6, A8, FINSEQ_1:def 3;
for i being Nat st i in Seg n holds
p1 . i = p2 . i

proof

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

end;

hence p1 = p2 by A10, 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