let x, y be FinSequence of REAL ; :: thesis: for M being Matrix of REAL st len x = len M & len y = width M holds
|((x * M),y)| = SumAll (QuadraticForm x,M,y)
let M be Matrix of REAL ; :: thesis: ( len x = len M & len y = width M implies |((x * M),y)| = SumAll (QuadraticForm x,M,y) )
set Z = QuadraticForm x,M,y;
assume that
A1: len x = len M and
A2: len y = width M ; :: thesis: |((x * M),y)| = SumAll (QuadraticForm x,M,y)
A3: len (QuadraticForm x,M,y) = len x by A1, A2, Def4;
A4: len (ColSum (QuadraticForm x,M,y)) = width (QuadraticForm x,M,y) by Def2;
len (x * M) = len y by A1, A2, MATRIXR1:62;
then A5: len (mlt (x * M),y) = len y by Th30
.= len (ColSum (QuadraticForm x,M,y)) by A1, A2, A4, Def4 ;
for i being Nat st 1 <= i & i <= len (ColSum (QuadraticForm x,M,y)) holds
(ColSum (QuadraticForm x,M,y)) . i = (mlt (x * M),y) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (ColSum (QuadraticForm x,M,y)) implies (ColSum (QuadraticForm x,M,y)) . i = (mlt (x * M),y) . i )
assume that
A6: 1 <= i and
A7: i <= len (ColSum (QuadraticForm x,M,y)) ; :: thesis: (ColSum (QuadraticForm x,M,y)) . i = (mlt (x * M),y) . i
A8: i in Seg (len (ColSum (QuadraticForm x,M,y))) by A6, A7, FINSEQ_1:3;
then A9: i in Seg (width M) by A1, A2, A4, Def4;
then A10: i in Seg (len (x * M)) by A1, MATRIXR1:62;
A11: len (Col M,i) = len x by A1, MATRIX_1:def 9;
A12: i <= width M by A9, FINSEQ_1:3;
A13: for j being Nat st 1 <= j & j <= len (Col (QuadraticForm x,M,y),i) holds
((y . i) * (mlt x,(Col M,i))) . j = (Col (QuadraticForm x,M,y),i) . j

proof

let j be Nat; :: thesis: ( 1 <= j & j <= len (Col (QuadraticForm x,M,y),i) implies ((y . i) * (mlt x,(Col M,i))) . j = (Col (QuadraticForm x,M,y),i) . j )
assume that
A14: 1 <= j and
A15: j <= len (Col (QuadraticForm x,M,y),i) ; :: thesis: ((y . i) * (mlt x,(Col M,i))) . j = (Col (QuadraticForm x,M,y),i) . j
j <= len M by A1, A3, A15, MATRIX_1:def 9;
then A16: [j,i] in Indices M by A6, A12, A14, MATRIXC1:1;
j in Seg (len (Col (QuadraticForm x,M,y),i)) by A14, A15, FINSEQ_1:3;
then A17: j in Seg (len (QuadraticForm x,M,y)) by MATRIX_1:def 9;
then A18: j in dom (QuadraticForm x,M,y) by FINSEQ_1:def 3;
A20: j in dom M by A1, A3, A17, FINSEQ_1:def 3;
thus ((y . i) * (mlt x,(Col M,i))) . j = (y . i) * ((mlt x,(Col M,i)) . j) by RVSUM_1:66
.= (y . i) * ((x . j) * ((Col M,i) . j)) by RVSUM_1:86
.= (y . i) * ((x . j) * (M * j,i)) by A20, MATRIX_1:def 9
.= (QuadraticForm x,M,y) * j,i by A1, A2, A16, Def4
.= (Col (QuadraticForm x,M,y),i) . j by A18, MATRIX_1:def 9 ; :: thesis: verum

end;

A21: len (Col (QuadraticForm x,M,y),i) = len x by A3, MATRIX_1:def 9;
len (mlt x,(Col M,i)) = len x by A11, Th30;
then len ((y . i) * (mlt x,(Col M,i))) = len (Col (QuadraticForm x,M,y),i) by A21, RVSUM_1:147;
then A22: (y . i) * (mlt x,(Col M,i)) = Col (QuadraticForm x,M,y),i by A13, FINSEQ_1:18;
(mlt (x * M),y) . i = ((x * M) . i) * (y . i) by RVSUM_1:86
.= (x "*" (Col M,i)) * (y . i) by A1, A10, Th40
.= Sum ((y . i) * (mlt x,(Col M,i))) by RVSUM_1:117 ;
hence (ColSum (QuadraticForm x,M,y)) . i = (mlt (x * M),y) . i by A4, A8, A22, Def2; :: thesis: verum

end;

hence |((x * M),y)| = Sum (ColSum (QuadraticForm x,M,y)) by A5, FINSEQ_1:18
.= SumAll (QuadraticForm x,M,y) by Th29 ;
:: thesis: verum