reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
defpred S₁[ Nat, set ] means for j being Nat st j = p . $1 holds
$2 = M * $1,j;
A1: for k being Nat st k in Seg n1 holds
ex x being Element of K st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg n1 implies ex x being Element of K st S₁[k,x] )
assume A2: k in Seg n1 ; :: thesis: ex x being Element of K st S₁[k,x]
reconsider p = p as Function of (Seg n),(Seg n) by MATRIX_2:def 11;
p . k in Seg n by A2, FUNCT_2:7;
then reconsider j = p . k as Element of NAT ;
reconsider x = M * k,j as Element of K ;
take x ; :: thesis: S₁[k,x]
thus S₁[k,x] ; :: thesis: verum

end;

consider t being FinSequence of K such that
A3: dom t = Seg n1 and
A4: for k being Nat st k in Seg n1 holds
S₁[k,t . k] from FINSEQ_1:sch 5(A1);
take t ; :: thesis: ( len t = n & ( for i, j being Nat st i in dom t & j = p . i holds
t . i = M * i,j ) )
thus len t = n by A3, FINSEQ_1:def 3; :: thesis: for i, j being Nat st i in dom t & j = p . i holds
t . i = M * i,j
let i, j be Nat; :: thesis: ( i in dom t & j = p . i implies t . i = M * i,j )
assume A5: ( i in dom t & j = p . i ) ; :: thesis: t . i = M * i,j
thus t . i = M * i,j by A3, A4, A5; :: thesis: verum