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

proof

reconsider p = p as Function of (Seg n),(Seg n) by MATRIX_2:def 11;
let k be Nat; :: thesis: ( k in Seg n1 implies ex x being Element of K st S₁[k,x] )
assume k in Seg n1 ; :: thesis: ex x being Element of K st S₁[k,x]
then p . k in Seg n by 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
A2: dom t = Seg n1 and
A3: 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 A2, 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 ( i in dom t & j = p . i ) ; :: thesis: t . i = M * i,j
hence t . i = M * i,j by A2, A3; :: thesis: verum