let m, n be Nat; :: thesis: for V1 being free finite-rank Z_Module
for M being Matrix of n,m,INT.Ring st n > 0 & m > 0 holds
for p, d being FinSequence of INT.Ring st len p = n & len d = m & ( for j being Nat st j in dom d holds
d /. j = Sum (mlt (p,(Col (M,j)))) ) holds
for b, c being FinSequence of V1 st len b = m & len c = n & ( for i being Nat st i in dom c holds
c /. i = Sum (lmlt ((Line (M,i)),b)) ) holds
Sum (lmlt (p,c)) = Sum (lmlt (d,b))
let V1 be free finite-rank Z_Module; :: thesis: for M being Matrix of n,m,INT.Ring st n > 0 & m > 0 holds
for p, d being FinSequence of INT.Ring st len p = n & len d = m & ( for j being Nat st j in dom d holds
d /. j = Sum (mlt (p,(Col (M,j)))) ) holds
for b, c being FinSequence of V1 st len b = m & len c = n & ( for i being Nat st i in dom c holds
c /. i = Sum (lmlt ((Line (M,i)),b)) ) holds
Sum (lmlt (p,c)) = Sum (lmlt (d,b))
let M be Matrix of n,m,INT.Ring; :: thesis: ( n > 0 & m > 0 implies for p, d being FinSequence of INT.Ring st len p = n & len d = m & ( for j being Nat st j in dom d holds
d /. j = Sum (mlt (p,(Col (M,j)))) ) holds
for b, c being FinSequence of V1 st len b = m & len c = n & ( for i being Nat st i in dom c holds
c /. i = Sum (lmlt ((Line (M,i)),b)) ) holds
Sum (lmlt (p,c)) = Sum (lmlt (d,b)) )
assume that
A1: n > 0 and
A2: m > 0 ; :: thesis: for p, d being FinSequence of INT.Ring st len p = n & len d = m & ( for j being Nat st j in dom d holds
d /. j = Sum (mlt (p,(Col (M,j)))) ) holds
for b, c being FinSequence of V1 st len b = m & len c = n & ( for i being Nat st i in dom c holds
c /. i = Sum (lmlt ((Line (M,i)),b)) ) holds
Sum (lmlt (p,c)) = Sum (lmlt (d,b))
A3: len M = n by A1, MATRIX_0:23;
reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 12;
let p, d be FinSequence of INT.Ring; :: thesis: ( len p = n & len d = m & ( for j being Nat st j in dom d holds
d /. j = Sum (mlt (p,(Col (M,j)))) ) implies for b, c being FinSequence of V1 st len b = m & len c = n & ( for i being Nat st i in dom c holds
c /. i = Sum (lmlt ((Line (M,i)),b)) ) holds
Sum (lmlt (p,c)) = Sum (lmlt (d,b)) )
assume that
A4: len p = n and
A5: len d = m and
A6: for j being Nat st j in dom d holds
d /. j = Sum (mlt (p,(Col (M,j)))) ; :: thesis: for b, c being FinSequence of V1 st len b = m & len c = n & ( for i being Nat st i in dom c holds
c /. i = Sum (lmlt ((Line (M,i)),b)) ) holds
Sum (lmlt (p,c)) = Sum (lmlt (d,b))
let b, c be FinSequence of V1; :: thesis: ( len b = m & len c = n & ( for i being Nat st i in dom c holds
c /. i = Sum (lmlt ((Line (M,i)),b)) ) implies Sum (lmlt (p,c)) = Sum (lmlt (d,b)) )
assume that
A7: len b = m and
A8: len c = n and
A9: for i being Nat st i in dom c holds
c /. i = Sum (lmlt ((Line (M,i)),b)) ; :: thesis: Sum (lmlt (p,c)) = Sum (lmlt (d,b))
deffunc H₁( Nat, Nat) -> Element of the carrier of V1 = ((p /. $1) * (M * ($1,$2))) * (b /. $2);
consider M1 being Matrix of n1,m1, the carrier of V1 such that
A10: for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = H₁(i,j) from MATRIX_0:sch 1();
A11: width M1 = len (M1 @) by MATRIX_0:def 6
.= len (Sum (M1 @)) by MATRLIN:def 6 ;
A12: dom d = dom b by A5, A7, FINSEQ_3:29;
then A13: dom (lmlt (d,b)) = dom b by Th12;
then A14: len (lmlt (d,b)) = len b by FINSEQ_3:29
.= len (Sum (M1 @)) by A1, A7, A11, MATRIX_0:23 ;
then A15: dom (lmlt (d,b)) = Seg (len (Sum (M1 @))) by FINSEQ_1:def 3;
A16: width M1 = m by A1, MATRIX_0:23;
A17: len M1 = n by A1, MATRIX_0:23;

A19: now :: thesis: for j being Nat st j in dom (lmlt (d,b)) holds
(lmlt (d,b)) . j = (Sum (M1 @)) . j

A20: Seg (len (Sum (M1 @))) = dom (Sum (M1 @)) by FINSEQ_1:def 3;
let j be Nat; :: thesis: ( j in dom (lmlt (d,b)) implies (lmlt (d,b)) . j = (Sum (M1 @)) . j )
assume A21: j in dom (lmlt (d,b)) ; :: thesis: (lmlt (d,b)) . j = (Sum (M1 @)) . j
A22: j in dom (Sum (M1 @)) by A15, A21, FINSEQ_1:def 3;
A23: j in dom d by A12, A21, Th12;
A24: ( d /. j = d . j & b /. j = b . j ) by A12, A13, A21, PARTFUN1:def 6;
len (Sum (M1 @)) = len (M1 @) by MATRLIN:def 6;
then A25: dom (Sum (M1 @)) = dom (M1 @) by FINSEQ_3:29;
then A26: (M1 @) /. j = (M1 @) . j by A22, PARTFUN1:def 6
.= Line ((M1 @),j) by A22, A25, MATRIX_0:60 ;
reconsider H = mlt (p,(Col (M,j))) as FinSequence of INT.Ring ;
deffunc H₂( Nat) -> Element of the carrier of V1 = (H /. $1) * (b /. j);
consider G being FinSequence of V1 such that
A27: ( len G = len p & ( for i being Nat st i in dom G holds
G . i = H₂(i) ) ) from FINSEQ_2:sch 1();
A28: len p = len (Col (M,j)) by A4, A3, MATRIX_0:def 8;
then A29: len ( the multF of INT.Ring .: (p,(Col (M,j)))) = len p by FINSEQ_2:72;
then A30: dom H = dom G by A27, FINSEQ_3:29;
A31: dom p = dom G by A27, FINSEQ_3:29;
A32: len (Line ((M1 @),j)) = width (M1 @) by MATRIX_0:def 7
.= len ((M1 @) @) by MATRIX_0:def 6
.= len G by A1, A2, A4, A17, A16, A27, MATRIX_0:57 ;
then A33: dom (Line ((M1 @),j)) = Seg (len G) by FINSEQ_1:def 3;
A34: dom G = Seg (len p) by A27, FINSEQ_1:def 3;

A35: now :: thesis: for i being Nat st i in dom (Line ((M1 @),j)) holds
(Line ((M1 @),j)) . i = G . i

let i be Nat; :: thesis: ( i in dom (Line ((M1 @),j)) implies (Line ((M1 @),j)) . i = G . i )
A36: dom M = Seg (len M) by FINSEQ_1:def 3;
assume A37: i in dom (Line ((M1 @),j)) ; :: thesis: (Line ((M1 @),j)) . i = G . i
then A38: i in Seg (len ( the multF of INT.Ring .: (p,(Col (M,j))))) by A27, A28, A33, FINSEQ_2:72;
then A39: i in dom H by FINSEQ_1:def 3;
A40: i in dom (multint .: (p,(Col (M,j)))) by A38, FINSEQ_1:def 3;
A41: Seg (len G) = dom G by FINSEQ_1:def 3;
then p /. i = p . i by A31, A33, A37, PARTFUN1:def 6;
then A42: (p /. i) * (M * (i,j)) = multint . ((p . i),((Col (M,j)) . i)) by A4, A3, A27, A33, A37, A36, MATRIX_0:def 8
.= (multint .: (p,(Col (M,j)))) . i by A40, FUNCOP_1:22
.= H /. i by A39, PARTFUN1:def 6 ;
dom M1 = dom G by A4, A17, A27, FINSEQ_3:29;
then A43: [i,j] in Indices M1 by A11, A15, A21, A33, A37, A41, ZFMISC_1:87;
i in Seg (width (M1 @)) by A32, A33, A37, MATRIX_0:def 7;
hence (Line ((M1 @),j)) . i = (M1 @) * (j,i) by MATRIX_0:def 7
.= M1 * (i,j) by A43, MATRIX_0:def 6
.= (H /. i) * (b /. j) by A10, A43, A42
.= G . i by A27, A34, A33, A37 ;
:: thesis: verum

end;

thus (lmlt (d,b)) . j = the lmult of V1 . ((d . j),(b . j)) by A21, FUNCOP_1:22
.= (Sum H) * (b /. j) by A6, A23, A24
.= Sum G by A27, A29, A30, Th10
.= Sum ((M1 @) /. j) by A32, A35, A26, FINSEQ_2:9
.= (Sum (M1 @)) /. j by A22, MATRLIN:def 6
.= (Sum (M1 @)) . j by A15, A21, A20, PARTFUN1:def 6 ; :: thesis: verum

end;

A44: dom p = dom c by A4, A8, FINSEQ_3:29;
then A45: dom (lmlt (p,c)) = dom p by Th12;
then A46: len (lmlt (p,c)) = len p by FINSEQ_3:29
.= len M1 by A4, MATRIX_0:def 2
.= len (Sum M1) by MATRLIN:def 6 ;

now :: thesis: for i being Nat st i in dom (Sum M1) holds
(lmlt (p,c)) . i = (Sum M1) . i

let i be Nat; :: thesis: ( i in dom (Sum M1) implies (lmlt (p,c)) . i = (Sum M1) . i )
assume A47: i in dom (Sum M1) ; :: thesis: (lmlt (p,c)) . i = (Sum M1) . i
A48: i in dom c by A44, A45, A46, A47, FINSEQ_3:29;
then A49: ( c . i = c /. i & p . i = p /. i ) by A44, PARTFUN1:def 6;
i in Seg (len (Sum M1)) by A47, FINSEQ_1:def 3;
then i in Seg (len M1) by MATRLIN:def 6;
then A50: i in dom M1 by FINSEQ_1:def 3;
then A51: M1 /. i = M1 . i by PARTFUN1:def 6
.= Line (M1,i) by A50, MATRIX_0:60 ;
deffunc H₂( Nat) -> Element of the carrier of V1 = (p /. i) * ((lmlt ((Line (M,i)),b)) /. $1);
consider F being FinSequence of V1 such that
A52: ( len F = len b & ( for j being Nat st j in dom F holds
F . j = H₂(j) ) ) from FINSEQ_2:sch 1();
A53: len F = width M by A1, A7, A52, MATRIX_0:23;
A54: dom (Line (M,i)) = Seg (len (Line (M,i))) by FINSEQ_1:def 3
.= dom b by A52, A53, FINSEQ_1:def 3, MATRIX_0:def 7 ;
then dom (lmlt ((Line (M,i)),b)) = dom b by Th12;
then A55: ( len F = len (lmlt ((Line (M,i)),b)) & dom F = dom (lmlt ((Line (M,i)),b)) ) by A52, FINSEQ_3:29;
A56: len F = width M1 by A1, A7, A52, MATRIX_0:23;
then A57: len (Line (M1,i)) = len F by MATRIX_0:def 7;
then A58: dom (M1 /. i) = Seg (len F) by A51, FINSEQ_1:def 3;
A59: dom F = Seg (len b) by A52, FINSEQ_1:def 3;

A60: now :: thesis: for j being Nat st j in dom (M1 /. i) holds
(M1 /. i) . j = F . j

let j be Nat; :: thesis: ( j in dom (M1 /. i) implies (M1 /. i) . j = F . j )
assume A61: j in dom (M1 /. i) ; :: thesis: (M1 /. i) . j = F . j
then A62: (Line (M,i)) . j = M * (i,j) by A53, A58, MATRIX_0:def 7;
A63: [i,j] in Indices M1 by A56, A50, A58, A61, ZFMISC_1:87;
A64: j in dom b by A52, A58, A61, FINSEQ_1:def 3;
then A65: b . j = b /. j by PARTFUN1:def 6;
A66: j in dom (lmlt ((Line (M,i)),b)) by A54, A64, Th12;
then A67: (lmlt ((Line (M,i)),b)) /. j = (lmlt ((Line (M,i)),b)) . j by PARTFUN1:def 6
.= (M * (i,j)) * (b /. j) by A65, A62, A66, FUNCOP_1:22 ;
thus (M1 /. i) . j = M1 * (i,j) by A56, A51, A58, A61, MATRIX_0:def 7
.= ((p /. i) * (M * (i,j))) * (b /. j) by A10, A63
.= (p /. i) * ((lmlt ((Line (M,i)),b)) /. j) by A67, VECTSP_1:def 16
.= F . j by A52, A59, A58, A61 ; :: thesis: verum

end;

A68: for j being Nat
for v being Vector of V1 st j in dom F & v = (lmlt ((Line (M,i)),b)) . j holds
F . j = (p /. i) * v

proof

let j be Nat; :: thesis: for v being Vector of V1 st j in dom F & v = (lmlt ((Line (M,i)),b)) . j holds
F . j = (p /. i) * v
let v be Vector of V1; :: thesis: ( j in dom F & v = (lmlt ((Line (M,i)),b)) . j implies F . j = (p /. i) * v )
assume A681: ( j in dom F & v = (lmlt ((Line (M,i)),b)) . j ) ; :: thesis: F . j = (p /. i) * v
thus F . j = (p /. i) * ((lmlt ((Line (M,i)),b)) /. j) by A52, A681
.= (p /. i) * v by A55, A681, PARTFUN1:def 6 ; :: thesis: verum

end;

i in dom ( the lmult of V1 .: (p,c)) by A46, A47, FINSEQ_3:29;
hence (lmlt (p,c)) . i = the lmult of V1 . ((p . i),(c . i)) by FUNCOP_1:22
.= (p /. i) * (Sum (lmlt ((Line (M,i)),b))) by A9, A48, A49
.= Sum F by A55, A68, ZMODUL01:12
.= Sum (M1 /. i) by A57, A51, A60, FINSEQ_2:9
.= (Sum M1) /. i by A47, MATRLIN:def 6
.= (Sum M1) . i by A47, PARTFUN1:def 6 ;
:: thesis: verum

end;

hence Sum (lmlt (p,c)) = Sum (Sum M1) by A46, FINSEQ_2:9
.= Sum (Sum (M1 @)) by Th32
.= Sum (lmlt (d,b)) by A14, A19, FINSEQ_2:9 ;
:: thesis: verum