defpred S_{1}[ 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_{1}[i,j,x]

A3: for i, j being Nat st [i,j] in Indices M holds

S_{1}[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)

M * (i,1) = p . (i - 1) ; :: thesis: verum

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

proof

consider M being Matrix of m9,1,L such that
let i, j be Nat; :: thesis: ( [i,j] in [:(Seg m9),(Seg 1):] implies ex x being Element of L st S_{1}[i,j,x] )

assume A2: [i,j] in [:(Seg m9),(Seg 1):] ; :: thesis: ex x being Element of L st S_{1}[i,j,x]

take p /. (i - 1) ; :: thesis: S_{1}[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_{1}[i,j,p /. (i - 1)]
by INT_1:3, PARTFUN1:def 6; :: thesis: verum

end;assume A2: [i,j] in [:(Seg m9),(Seg 1):] ; :: thesis: ex x being Element of L st S

take p /. (i - 1) ; :: thesis: S

[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

A3: for i, j being Nat st [i,j] in Indices M holds

S

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)

hence
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;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

M * (i,1) = p . (i - 1) ; :: thesis: verum