reconsider m' = m as Element of NAT by ORDINAL1:def 13;
defpred S₁[ Nat, set , set ] means $3 = p . ($1 - 1);
A1: for i, j being Nat st [i,j] in [:(Seg m'),(Seg 1):] holds
for x1, x2 being Element of L st S₁[i,j,x1] & S₁[i,j,x2] holds
x1 = x2 ;
A2: for i, j being Nat st [i,j] in [:(Seg m'),(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 m'),(Seg 1):] implies ex x being Element of L st S₁[i,j,x] )
assume A3: [i,j] in [:(Seg m'),(Seg 1):] ; :: thesis: ex x being Element of L st S₁[i,j,x]
take x = p /. (i - 1); :: thesis: S₁[i,j,x]
A4: dom p = NAT by FUNCT_2:def 1;
[i,j] `1 in Seg m by A3, MCART_1:10;
then i in Seg m by MCART_1:def 1;
then 1 <= i by FINSEQ_1:3;
then 1 - 1 <= i - 1 by XREAL_1:11;
hence S₁[i,j,x] by A4, INT_1:16, PARTFUN1:def 8; :: thesis: verum

end;

consider M being Matrix of m',1,L such that
A5: for i, j being Nat st [i,j] in Indices M holds
S₁[i,j,M * i,j] from MATRIX_1:sch 2(A1, A2);
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

let i be Nat; :: thesis: ( 1 <= i & i <= m implies M * i,1 = p . (i - 1) )
assume A6: ( 1 <= i & i <= m ) ; :: thesis: M * i,1 = p . (i - 1)
then A7: i in Seg m by FINSEQ_1:3;
A8: 1 in Seg 1 ;
Indices M = [:(Seg m),(Seg 1):] by A6, MATRIX_1:24;
then [i,1] in Indices M by A7, A8, ZFMISC_1:def 2;
hence M * i,1 = p . (i - 1) by A5; :: thesis: verum

end;

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