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 12;
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_1:def 12;
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:5;
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