let n, m 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 A1, MATRIX_1:24;
reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 13;
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 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_1:sch 1();
A11: width M1 = len (M1 @ ) by MATRIX_1:def 7
.= len (Sum (M1 @ )) by Def8 ;
A12: dom d = dom b by A5, A7, FINSEQ_3:31;
then A13: dom (lmlt d,b) = dom b by Th16;
then A14: len (lmlt d,b) = len b by FINSEQ_3:31
.= len (Sum (M1 @ )) by A1, A7, A11, MATRIX_1:24 ;
then A15: dom (lmlt d,b) = Seg (len (Sum (M1 @ ))) by FINSEQ_1:def 3;
A16: width M1 = m by A1, MATRIX_1:24;
A17: len M1 = n by A1, MATRIX_1:24;
A18: dom (lmlt d,b) = dom d by A12, Th16;

A19: now

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, Th16;
A24: ( d /. j = d . j & b /. j = b . j ) by A18, A13, A21, PARTFUN1:def 8;
len (Sum (M1 @ )) = len (M1 @ ) by Def8;
then A25: dom (Sum (M1 @ )) = dom (M1 @ ) by FINSEQ_3:31;
then A26: (M1 @ ) /. j = (M1 @ ) . j by A22, PARTFUN1:def 8
.= Line (M1 @ ),j by A22, A25, MATRIX_2:18 ;
reconsider H = mlt p,(Col M,j) as FinSequence of K ;
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_1:def 9;
then A29: len (the multF of K .: p,(Col M,j)) = len p by FINSEQ_2:86;
then A30: dom H = dom G by A27, FINSEQ_3:31;
A31: dom p = dom G by A27, FINSEQ_3:31;
A32: len (Line (M1 @ ),j) = width (M1 @ ) by MATRIX_1:def 8
.= len ((M1 @ ) @ ) by MATRIX_1:def 7
.= len G by A1, A2, A4, A17, A16, A27, MATRIX_2:15 ;
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

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 A27, A28, A33, FINSEQ_2:86;
then A39: i in dom H by FINSEQ_1:def 3;
A40: i in dom (the multF of K .: p,(Col M,j)) by A38, FINSEQ_1:def 3;
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 A31, A33, A37, PARTFUN1:def 8
.= the multF of K . (p . i),((Col M,j) . i) by A4, A3, A27, A33, A37, A36, MATRIX_1:def 9
.= (the multF of K .: p,(Col M,j)) . i by A40, FUNCOP_1:28
.= H /. i by A39, PARTFUN1:def 8 ;
dom M1 = dom G by A4, A17, A27, FINSEQ_3:31;
then [i,j] in [:(dom M1),(Seg (width M1)):] by A11, A15, A21, A33, A37, A41, ZFMISC_1:106;
then A43: [i,j] in Indices M1 by MATRIX_1:def 5;
i in Seg (width (M1 @ )) by A32, A33, A37, MATRIX_1:def 8;
hence (Line (M1 @ ),j) . i = (M1 @ ) * j,i by MATRIX_1:def 8
.= M1 * i,j by A43, MATRIX_1:def 7
.= (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:28
.= (d /. j) * (b /. j) by A24, VECTSP_1:def 24
.= (Sum H) * (b /. j) by A6, A23
.= Sum G by A27, A29, A30, Th14
.= Sum ((M1 @ ) /. j) by A32, A35, A26, FINSEQ_2:10
.= (Sum (M1 @ )) /. j by A22, Def8
.= (Sum (M1 @ )) . j by A15, A21, A20, PARTFUN1:def 8 ; :: thesis: verum

end;

A44: dom p = dom c by A4, A8, FINSEQ_3:31;
then A45: dom (lmlt p,c) = dom p by Th16;
then A46: len (lmlt p,c) = len p by FINSEQ_3:31
.= len M1 by A4, MATRIX_1:def 3
.= len (Sum M1) by Def8 ;

now

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:31;
then A49: ( c . i = c /. i & p . i = p /. i ) by A44, PARTFUN1:def 8;
i in Seg (len (Sum M1)) by A47, FINSEQ_1:def 3;
then i in Seg (len M1) by Def8;
then A50: i in dom M1 by FINSEQ_1:def 3;
then A51: M1 /. i = M1 . i by PARTFUN1:def 8
.= Line M1,i by A50, MATRIX_2:18 ;
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_1:24;
A54: dom (Line M,i) = Seg (len (Line M,i)) by FINSEQ_1:def 3
.= Seg (len F) by A53, MATRIX_1:def 8
.= dom b by A52, FINSEQ_1:def 3 ;
then dom (lmlt (Line M,i),b) = dom b by Th16;
then A55: ( len F = len (lmlt (Line M,i),b) & dom F = dom (lmlt (Line M,i),b) ) by A52, FINSEQ_3:31;
A56: len F = width M1 by A1, A7, A52, MATRIX_1:24;
then A57: len (Line M1,i) = len F by MATRIX_1:def 8;
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

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_1:def 8;
[i,j] in [:(dom M1),(Seg (width M1)):] by A56, A50, A58, A61, ZFMISC_1:106;
then A63: [i,j] in Indices M1 by MATRIX_1:def 5;
A64: j in dom b by A52, A58, A61, FINSEQ_1:def 3;
then A65: b . j = b /. j by PARTFUN1:def 8;
A66: j in dom (lmlt (Line M,i),b) by A54, A64, Th16;
then A67: (lmlt (Line M,i),b) /. j = (lmlt (Line M,i),b) . j by PARTFUN1:def 8
.= the lmult of V1 . ((Line M,i) . j),(b . j) by A66, FUNCOP_1:28
.= (M * i,j) * (b /. j) by A65, A62, VECTSP_1:def 24 ;
thus (M1 /. i) . j = M1 * i,j by A56, A51, A58, A61, MATRIX_1:def 8
.= ((p /. i) * (M * i,j)) * (b /. j) by A10, A63
.= (p /. i) * ((lmlt (Line M,i),b) /. j) by A67, VECTSP_1:def 28
.= F . j by A52, A59, A58, A61 ; :: thesis: verum

end;

A68: for j being Element of 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 A46, A47, FINSEQ_3:31;
hence (lmlt p,c) . i = the lmult of V1 . (p . i),(c . i) by FUNCOP_1:28
.= (p /. i) * (c /. i) by A49, VECTSP_1:def 24
.= (p /. i) * (Sum (lmlt (Line M,i),b)) by A9, A48
.= Sum F by A55, A68, VECTSP_3:10
.= Sum (M1 /. i) by A57, A51, A60, FINSEQ_2:10
.= (Sum M1) /. i by A47, Def8
.= (Sum M1) . i by A47, PARTFUN1:def 8 ;
:: thesis: verum

end;

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