let m, n be Nat; :: thesis: for K being Field
for V1 being finite-dimensional VectSp of K
for M being Matrix of n,m, the carrier of K st n > 0 & m > 0 holds
for p, d being FinSequence of K 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 K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for M being Matrix of n,m, the carrier of K st n > 0 & m > 0 holds
for p, d being FinSequence of K 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 finite-dimensional VectSp of K; :: thesis: for M being Matrix of n,m, the carrier of K st n > 0 & m > 0 holds
for p, d being FinSequence of K 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, the carrier of K; :: thesis: ( n > 0 & m > 0 implies for p, d being FinSequence of K 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 K 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 ;
reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 12;
let p, d be FinSequence of K; :: 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 H1( 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) = H1(i,j) from A11: width M1 = len (M1 @) by MATRIX_0:def 6
.= len (Sum (M1 @)) by Def6 ;
A12: dom d = dom b by ;
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 ;
then A15: dom (lmlt (d,b)) = Seg (len (Sum (M1 @))) by FINSEQ_1:def 3;
A16: width M1 = m by ;
A17: len M1 = n by ;
A18: dom (lmlt (d,b)) = dom d by ;
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 ;
A23: j in dom d by ;
A24: ( d /. j = d . j & b /. j = b . j ) by ;
len (Sum (M1 @)) = len (M1 @) by Def6;
then A25: dom (Sum (M1 @)) = dom (M1 @) by FINSEQ_3:29;
then A26: (M1 @) /. j = (M1 @) . j by
.= Line ((M1 @),j) by ;
reconsider H = mlt (p,(Col (M,j))) as FinSequence of K ;
deffunc H2( 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 = H2(i) ) ) from A28: len p = len (Col (M,j)) by ;
then A29: len ( the multF of K .: (p,(Col (M,j)))) = len p by FINSEQ_2:72;
then A30: dom H = dom G by ;
A31: dom p = dom G by ;
A32: len (Line ((M1 @),j)) = width (M1 @) by MATRIX_0:def 7
.= len ((M1 @) @) by MATRIX_0:def 6
.= len G by ;
then A33: dom (Line ((M1 @),j)) = Seg (len G) by FINSEQ_1:def 3;
A34: dom G = Seg (len p) by ;
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 K .: (p,(Col (M,j))))) by ;
then A39: i in dom H by FINSEQ_1:def 3;
A40: i in dom ( the multF of K .: (p,(Col (M,j)))) by ;
A41: Seg (len G) = dom G by FINSEQ_1:def 3;
then A42: (p /. i) * (M * (i,j)) = the multF of K . ((p . i),(M * (i,j))) by
.= the multF of K . ((p . i),((Col (M,j)) . i)) by
.= ( the multF of K .: (p,(Col (M,j)))) . i by
.= H /. i by ;
dom M1 = dom G by ;
then [i,j] in [:(dom M1),(Seg (width M1)):] by ;
then A43: [i,j] in Indices M1 by MATRIX_0:def 4;
i in Seg (width (M1 @)) by ;
hence (Line ((M1 @),j)) . i = (M1 @) * (j,i) by MATRIX_0:def 7
.= M1 * (i,j) by
.= (H /. i) * (b /. j) by
.= G . i by A27, A34, A33, A37 ;
:: thesis: verum
end;
thus (lmlt (d,b)) . j = the lmult of V1 . ((d . j),(b . j)) by
.= (d /. j) * (b /. j) by
.= (Sum H) * (b /. j) by
.= Sum G by
.= Sum ((M1 @) /. j) by
.= (Sum (M1 @)) /. j by
.= (Sum (M1 @)) . j by ; :: thesis: verum
end;
A44: dom p = dom c by ;
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
.= len (Sum M1) by Def6 ;
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 ;
then A49: ( c . i = c /. i & p . i = p /. i ) by ;
i in Seg (len (Sum M1)) by ;
then i in Seg (len M1) by Def6;
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 ;
deffunc H2( 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 = H2(j) ) ) from A53: len F = width M by ;
A54: dom (Line (M,i)) = Seg (len (Line (M,i))) by FINSEQ_1:def 3
.= Seg (len F) by
.= dom b by ;
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 ;
A56: len F = width M1 by ;
then A57: len (Line (M1,i)) = len F by MATRIX_0:def 7;
then A58: dom (M1 /. i) = Seg (len F) by ;
A59: dom F = Seg (len b) by ;
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 ;
[i,j] in [:(dom M1),(Seg (width M1)):] by ;
then A63: [i,j] in Indices M1 by MATRIX_0:def 4;
A64: j in dom b by ;
then A65: b . j = b /. j by PARTFUN1:def 6;
A66: j in dom (lmlt ((Line (M,i)),b)) by ;
then A67: (lmlt ((Line (M,i)),b)) /. j = (lmlt ((Line (M,i)),b)) . j by PARTFUN1:def 6
.= the lmult of V1 . (((Line (M,i)) . j),(b . j)) by
.= (M * (i,j)) * (b /. j) by ;
thus (M1 /. i) . j = M1 * (i,j) by
.= ((p /. i) * (M * (i,j))) * (b /. j) by
.= (p /. i) * ((lmlt ((Line (M,i)),b)) /. j) by
.= F . j by A52, A59, A58, A61 ; :: thesis: verum
end;
A68: for j being Nat st j in dom F holds
F . j = (p /. i) * ((lmlt ((Line (M,i)),b)) /. j) by A52;
i in dom ( the lmult of V1 .: (p,c)) by ;
hence (lmlt (p,c)) . i = the lmult of V1 . ((p . i),(c . i)) by FUNCOP_1:22
.= (p /. i) * (c /. i) by
.= (p /. i) * (Sum (lmlt ((Line (M,i)),b))) by
.= Sum F by
.= Sum (M1 /. i) by
.= (Sum M1) /. i by
.= (Sum M1) . i by ;
:: thesis: verum
end;
hence Sum (lmlt (p,c)) = Sum (Sum M1) by
.= Sum (Sum (M1 @)) by Th32
.= Sum (lmlt (d,b)) by ;
:: thesis: verum