let n, m be Nat; :: thesis:
let K be Field; :: thesis:
let V1 be finite-dimensional VectSp of K; :: thesis:
let M be Matrix of n,m,the carrier of K; :: thesis:
assume A1: ( n > 0 & m > 0 ) ; :: thesis:
let p, d be FinSequence of K; :: thesis:
assume A2: ( len p = n & len d = m & ( for j being Nat st j in dom d holds
d /. j = Sum (mlt p,(Col M,j)) ) ) ; :: thesis:
let b, c be FinSequence of V1; :: thesis:
assume A3: ( len b = m & len c = n & ( for i being Nat st i in dom c holds
c /. i = Sum (lmlt (Line M,i),b) ) ) ; :: thesis:
deffunc H₁( Nat, Nat) -> Element of the carrier of V1 = ((p /. $1) * (M * $1,$2)) * (b /. $2);
reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 13;
consider M1 being Matrix of n1,m1,the carrier of V1 such that
A4: for i, j being Nat st [i,j] in Indices M1 holds
M1 * i,j = H₁(i,j) from MATRIX_1:sch 1();
A5: len M1 = n by A1, MATRIX_1:24;
A6: width M1 = m by A1, MATRIX_1:24;
A7: len M = n by A1, MATRIX_1:24;
A8: dom p = dom c by A2, A3, FINSEQ_3:31;
then A9: dom (lmlt p,c) = dom p by Th16;
then A10: len (lmlt p,c) = len p by FINSEQ_3:31
.= len M1 by A2, MATRIX_1:def 3
.= len (Sum M1) by Def8 ;

A11: now

let i be Nat; :: thesis:
assume A12: i in dom (Sum M1) ; :: thesis:
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
A13: ( len F = len b & ( for j being Nat st j in dom F holds
F . j = H₂(j) ) ) from FINSEQ_2:sch 1();
A14: dom F = Seg (len b) by A13, FINSEQ_1:def 3;
A15: len F = width M1 by A1, A3, A13, MATRIX_1:24;
A16: len F = width M by A1, A3, A13, MATRIX_1:24;
A17: len (Line M1,i) = len F by A15, MATRIX_1:def 8;
A18: dom (Line M,i) = Seg (len (Line M,i)) by FINSEQ_1:def 3
.= Seg (len F) by A16, MATRIX_1:def 8
.= dom b by A13, FINSEQ_1:def 3 ;
i in Seg (len (Sum M1)) by A12, FINSEQ_1:def 3;
then i in Seg (len M1) by Def8;
then A19: i in dom M1 by FINSEQ_1:def 3;
then A20: M1 /. i = M1 . i by PARTFUN1:def 8
.= Line M1,i by A19, MATRIX_2:18 ;
X: dom (M1 /. i) = Seg (len F) by A20, A17, FINSEQ_1:def 3;

A21: now

let j be Nat; :: thesis:
assume A22: j in dom (M1 /. i) ; :: thesis:
then A23: j in dom b by A13, X, FINSEQ_1:def 3;
then A24: j in dom (lmlt (Line M,i),b) by A18, Th16;
A25: b . j = b /. j by A23, PARTFUN1:def 8;
A26: (Line M,i) . j = M * i,j by A16, A22, X, MATRIX_1:def 8;
[i,j] in [:(dom M1),(Seg (width M1)):] by A15, A19, A22, X, ZFMISC_1:106;
then A27: [i,j] in Indices M1 by MATRIX_1:def 5;
A28: (lmlt (Line M,i),b) /. j = (lmlt (Line M,i),b) . j by A24, PARTFUN1:def 8
.= the lmult of V1 . ((Line M,i) . j),(b . j) by A24, FUNCOP_1:28
.= (M * i,j) * (b /. j) by A25, A26, VECTSP_1:def 24 ;
thus (M1 /. i) . j = M1 * i,j by A15, A20, A22, X, MATRIX_1:def 8
.= ((p /. i) * (M * i,j)) * (b /. j) by A4, A27
.= (p /. i) * ((lmlt (Line M,i),b) /. j) by A28, VECTSP_1:def 26
.= F . j by A13, A22, A14, X ; :: thesis:

end;

A29: i in dom c by A8, A9, A10, A12, FINSEQ_3:31;
then A30: c . i = c /. i by PARTFUN1:def 8;
A31: p . i = p /. i by A8, A29, PARTFUN1:def 8;
A32: i in dom (the lmult of V1 .: p,c) by A10, A12, FINSEQ_3:31;
A33: dom (lmlt (Line M,i),b) = dom b by A18, Th16;
then A34: len F = len (lmlt (Line M,i),b) by A13, FINSEQ_3:31;
A35: dom F = dom (lmlt (Line M,i),b) by A13, A33, FINSEQ_3:31;
A36: for j being Element of NAT st j in dom F holds
F . j = (p /. i) * ((lmlt (Line M,i),b) /. j) by A13;
thus (lmlt p,c) . i = the lmult of V1 . (p . i),(c . i) by A32, FUNCOP_1:28
.= (p /. i) * (c /. i) by A30, A31, VECTSP_1:def 24
.= (p /. i) * (Sum (lmlt (Line M,i),b)) by A3, A29
.= Sum F by A34, A35, A36, VECTSP_3:10
.= Sum (M1 /. i) by A17, A20, A21, FINSEQ_2:10
.= (Sum M1) /. i by A12, Def8
.= (Sum M1) . i by A12, PARTFUN1:def 8 ; :: thesis:

end;

A37: dom d = dom b by A2, A3, FINSEQ_3:31;
then A38: dom (lmlt d,b) = dom d by Th16;
A39: dom (lmlt d,b) = dom b by A37, Th16;
A40: width M1 = len (M1 @ ) by MATRIX_1:def 7
.= len (Sum (M1 @ )) by Def8 ;
A41: len (lmlt d,b) = len b by A39, FINSEQ_3:31
.= len (Sum (M1 @ )) by A1, A3, A40, MATRIX_1:24 ;
Y: dom (lmlt d,b) = Seg (len (Sum (M1 @ ))) by A41, FINSEQ_1:def 3;

A42: now

let j be Nat; :: thesis:
assume A43: j in dom (lmlt d,b) ; :: thesis:
A44: Seg (len (Sum (M1 @ ))) = dom (Sum (M1 @ )) by FINSEQ_1:def 3;
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
A45: ( len G = len p & ( for i being Nat st i in dom G holds
G . i = H₂(i) ) ) from FINSEQ_2:sch 1();
A46: dom G = Seg (len p) by A45, FINSEQ_1:def 3;
A48: dom p = dom G by A45, FINSEQ_3:31;
A49: len (Line (M1 @ ),j) = width (M1 @ ) by MATRIX_1:def 8
.= len ((M1 @ ) @ ) by MATRIX_1:def 7
.= len G by A1, A2, A5, A6, A45, MATRIX_2:15 ;
A50: len p = len (Col M,j) by A2, A7, MATRIX_1:def 9;
then A51: len (the multF of K .: p,(Col M,j)) = len p by FINSEQ_2:86;
X: dom (Line (M1 @ ),j) = Seg (len G) by A49, FINSEQ_1:def 3;

A52: now

let i be Nat; :: thesis:
assume A53: i in dom (Line (M1 @ ),j) ; :: thesis:
then A54: i in Seg (width (M1 @ )) by A49, X, MATRIX_1:def 8;
A55: Seg (len G) = dom G by FINSEQ_1:def 3;
dom M1 = dom G by A2, A5, A45, FINSEQ_3:31;
then [i,j] in [:(dom M1),(Seg (width M1)):] by A40, A43, A53, A55, X, Y, ZFMISC_1:106;
then A56: [i,j] in Indices M1 by MATRIX_1:def 5;
A57: i in Seg (len (the multF of K .: p,(Col M,j))) by A45, A50, A53, X, FINSEQ_2:86;
then A58: i in dom H by FINSEQ_1:def 3;
A59: i in dom (the multF of K .: p,(Col M,j)) by A57, FINSEQ_1:def 3;
A60: dom M = Seg (len M) by FINSEQ_1:def 3;
A61: (p /. i) * (M * i,j) = the multF of K . (p . i),(M * i,j) by A48, A53, A55, X, PARTFUN1:def 8
.= the multF of K . (p . i),((Col M,j) . i) by A2, A7, A45, A53, A60, X, MATRIX_1:def 9
.= (the multF of K .: p,(Col M,j)) . i by A59, FUNCOP_1:28
.= H /. i by A58, PARTFUN1:def 8 ;
thus (Line (M1 @ ),j) . i = (M1 @ ) * j,i by A54, MATRIX_1:def 8
.= M1 * i,j by A56, MATRIX_1:def 7
.= (H /. i) * (b /. j) by A4, A56, A61
.= G . i by A45, A53, A46, X ; :: thesis:

end;

A62: j in dom (Sum (M1 @ )) by A43, Y, FINSEQ_1:def 3;
A63: j in dom (lmlt d,b) by A43;
then A64: d /. j = d . j by A38, PARTFUN1:def 8;
A65: b /. j = b . j by A39, A63, PARTFUN1:def 8;
A66: j in dom d by A37, A63, Th16;
A67: dom H = dom G by A45, A51, FINSEQ_3:31;
len (Sum (M1 @ )) = len (M1 @ ) by Def8;
then A68: dom (Sum (M1 @ )) = dom (M1 @ ) by FINSEQ_3:31;
then A69: (M1 @ ) /. j = (M1 @ ) . j by A62, PARTFUN1:def 8
.= Line (M1 @ ),j by A62, A68, MATRIX_2:18 ;
thus (lmlt d,b) . j = the lmult of V1 . (d . j),(b . j) by A63, FUNCOP_1:28
.= (d /. j) * (b /. j) by A64, A65, VECTSP_1:def 24
.= (Sum H) * (b /. j) by A2, A66
.= Sum G by A45, A51, A67, Th14
.= Sum ((M1 @ ) /. j) by A49, A52, A69, FINSEQ_2:10
.= (Sum (M1 @ )) /. j by A62, Def8
.= (Sum (M1 @ )) . j by A43, A44, Y, PARTFUN1:def 8 ; :: thesis:

end;

thus Sum (lmlt p,c) = Sum (Sum M1) by A10, A11, NEWTON:3
.= Sum (Sum (M1 @ )) by Th37
.= Sum (lmlt d,b) by A41, A42, FINSEQ_2:10 ; :: thesis: