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 A1, MATRIX_0:23;

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 H_{1}( 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_{1}(i,j)
from MATRIX_0:sch 1();

A11: width M1 = len (M1 @) by MATRIX_0:def 6

.= len (Sum (M1 @)) by Def6 ;

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;

A18: dom (lmlt (d,b)) = dom d by A12, Th12;

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

.= Sum (Sum (M1 @)) by Th32

.= Sum (lmlt (d,b)) by A14, A19, FINSEQ_2:9 ;

:: thesis: verum

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_0:23;

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 H

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

A11: width M1 = len (M1 @) by MATRIX_0:def 6

.= len (Sum (M1 @)) by Def6 ;

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;

A18: dom (lmlt (d,b)) = dom d by A12, Th12;

A19: now :: thesis: for j being Nat st j in dom (lmlt (d,b)) holds

(lmlt (d,b)) . j = (Sum (M1 @)) . j

A44:
dom p = dom c
by A4, A8, FINSEQ_3:29;(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 A18, A13, A21, PARTFUN1:def 6;

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 A22, PARTFUN1:def 6

.= Line ((M1 @),j) by A22, A25, MATRIX_0:60 ;

reconsider H = mlt (p,(Col (M,j))) as FinSequence of K ;

deffunc H_{2}( 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_{2}(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 K .: (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;

.= (d /. j) * (b /. j) by A24, VECTSP_1:def 12

.= (Sum H) * (b /. j) by A6, A23

.= Sum G by A27, A29, A30, Th10

.= Sum ((M1 @) /. j) by A32, A35, A26, FINSEQ_2:9

.= (Sum (M1 @)) /. j by A22, Def6

.= (Sum (M1 @)) . j by A15, A21, A20, PARTFUN1:def 6 ; :: thesis: verum

end;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 A18, A13, A21, PARTFUN1:def 6;

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 A22, PARTFUN1:def 6

.= Line ((M1 @),j) by A22, A25, MATRIX_0:60 ;

reconsider H = mlt (p,(Col (M,j))) as FinSequence of K ;

deffunc H

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

A28: len p = len (Col (M,j)) by A4, A3, MATRIX_0:def 8;

then A29: len ( the multF of K .: (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

thus (lmlt (d,b)) . j =
the lmult of V1 . ((d . j),(b . j))
by A21, FUNCOP_1:22
(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 A27, A28, A33, FINSEQ_2:72;

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 6

.= the multF of K . ((p . i),((Col (M,j)) . i)) by A4, A3, A27, A33, A37, A36, MATRIX_0:def 8

.= ( the multF of K .: (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 [i,j] in [:(dom M1),(Seg (width M1)):] by A11, A15, A21, A33, A37, A41, ZFMISC_1:87;

then A43: [i,j] in Indices M1 by MATRIX_0:def 4;

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;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:72;

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 6

.= the multF of K . ((p . i),((Col (M,j)) . i)) by A4, A3, A27, A33, A37, A36, MATRIX_0:def 8

.= ( the multF of K .: (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 [i,j] in [:(dom M1),(Seg (width M1)):] by A11, A15, A21, A33, A37, A41, ZFMISC_1:87;

then A43: [i,j] in Indices M1 by MATRIX_0:def 4;

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

.= (d /. j) * (b /. j) by A24, VECTSP_1:def 12

.= (Sum H) * (b /. j) by A6, A23

.= Sum G by A27, A29, A30, Th10

.= Sum ((M1 @) /. j) by A32, A35, A26, FINSEQ_2:9

.= (Sum (M1 @)) /. j by A22, Def6

.= (Sum (M1 @)) . j by A15, A21, A20, PARTFUN1:def 6 ; :: thesis: verum

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

now :: thesis: for i being Nat st i in dom (Sum M1) holds

(lmlt (p,c)) . i = (Sum M1) . i

hence Sum (lmlt (p,c)) =
Sum (Sum M1)
by A46, FINSEQ_2:9
(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 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 A50, MATRIX_0:60 ;

deffunc H_{2}( 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_{2}(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

.= Seg (len F) by A53, MATRIX_0:def 7

.= dom b by A52, FINSEQ_1:def 3 ;

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;

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:29;

hence (lmlt (p,c)) . i = the lmult of V1 . ((p . i),(c . i)) by FUNCOP_1:22

.= (p /. i) * (c /. i) by A49, VECTSP_1:def 12

.= (p /. i) * (Sum (lmlt ((Line (M,i)),b))) by A9, A48

.= Sum F by A55, A68, RLVECT_2:67

.= Sum (M1 /. i) by A57, A51, A60, FINSEQ_2:9

.= (Sum M1) /. i by A47, Def6

.= (Sum M1) . i by A47, PARTFUN1:def 6 ;

:: thesis: verum

end;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 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 A50, MATRIX_0:60 ;

deffunc H

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

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

.= Seg (len F) by A53, MATRIX_0:def 7

.= dom b by A52, FINSEQ_1:def 3 ;

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

A68:
for j being Nat st j in dom F 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;

[i,j] in [:(dom M1),(Seg (width M1)):] by A56, A50, A58, A61, ZFMISC_1:87;

then A63: [i,j] in Indices M1 by MATRIX_0:def 4;

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

.= the lmult of V1 . (((Line (M,i)) . j),(b . j)) by A66, FUNCOP_1:22

.= (M * (i,j)) * (b /. j) by A65, A62, VECTSP_1:def 12 ;

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

[i,j] in [:(dom M1),(Seg (width M1)):] by A56, A50, A58, A61, ZFMISC_1:87;

then A63: [i,j] in Indices M1 by MATRIX_0:def 4;

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

.= the lmult of V1 . (((Line (M,i)) . j),(b . j)) by A66, FUNCOP_1:22

.= (M * (i,j)) * (b /. j) by A65, A62, VECTSP_1:def 12 ;

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

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:29;

hence (lmlt (p,c)) . i = the lmult of V1 . ((p . i),(c . i)) by FUNCOP_1:22

.= (p /. i) * (c /. i) by A49, VECTSP_1:def 12

.= (p /. i) * (Sum (lmlt ((Line (M,i)),b))) by A9, A48

.= Sum F by A55, A68, RLVECT_2:67

.= Sum (M1 /. i) by A57, A51, A60, FINSEQ_2:9

.= (Sum M1) /. i by A47, Def6

.= (Sum M1) . i by A47, PARTFUN1:def 6 ;

:: thesis: verum

.= Sum (Sum (M1 @)) by Th32

.= Sum (lmlt (d,b)) by A14, A19, FINSEQ_2:9 ;

:: thesis: verum