defpred S₁[ Nat, set , set ] means $3 = p . ($1 - 1);
reconsider m9 = m as Element of NAT by ORDINAL1:def 12;
A1: for i, j being Nat st [i,j] in [:(Seg m9),(Seg 1):] holds
ex x being Element of L st S₁[i,j,x]

proof

let i, j be Nat; :: thesis: ( [i,j] in [:(Seg m9),(Seg 1):] implies ex x being Element of L st S₁[i,j,x] )
assume A2: [i,j] in [:(Seg m9),(Seg 1):] ; :: thesis: ex x being Element of L st S₁[i,j,x]
take p /. (i - 1) ; :: thesis: S₁[i,j,p /. (i - 1)]
[i,j] `1 in Seg m by A2, MCART_1:10;
then i in Seg m ;
then 1 <= i by FINSEQ_1:1;
then ( dom p = NAT & 1 - 1 <= i - 1 ) by FUNCT_2:def 1, XREAL_1:9;
hence S₁[i,j,p /. (i - 1)] by INT_1:3, PARTFUN1:def 6; :: thesis: verum

end;

consider M being Matrix of m9,1,L such that
A3: for i, j being Nat st [i,j] in Indices M holds
S₁[i,j,M * (i,j)] from MATRIX_0:sch 2(A1);
reconsider M = M as Matrix of m,1,L ;
take M ; :: thesis: for i being Nat st 1 <= i & i <= m holds
M * (i,1) = p . (i - 1)

now :: thesis: for i being Nat st 1 <= i & i <= m holds
M * (i,1) = p . (i - 1)

let i be Nat; :: thesis: ( 1 <= i & i <= m implies M * (i,1) = p . (i - 1) )
assume ( 1 <= i & i <= m ) ; :: thesis: M * (i,1) = p . (i - 1)
then A4: ( i in Seg m & Indices M = [:(Seg m),(Seg 1):] ) by MATRIX_0:23;
1 in Seg 1 ;
then [i,1] in Indices M by A4, ZFMISC_1:def 2;
hence M * (i,1) = p . (i - 1) by A3; :: thesis: verum

end;

hence for i being Nat st 1 <= i & i <= m holds
M * (i,1) = p . (i - 1) ; :: thesis: verum