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:1;
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 8;
A12: i <= width M by A9, FINSEQ_1:1;
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 8;
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:1;
then A17: j in Seg (len (QuadraticForm (x,M,y))) by MATRIX_1:def 8;
then A18: j in dom (QuadraticForm (x,M,y)) by FINSEQ_1:def 3;
A19: 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:44
.= (y . i) * ((x . j) * ((Col (M,i)) . j)) by RVSUM_1:59
.= (y . i) * ((x . j) * (M * (j,i))) by A19, MATRIX_1:def 8
.= (QuadraticForm (x,M,y)) * (j,i) by A1, A2, A16, Def4
.= (Col ((QuadraticForm (x,M,y)),i)) . j by A18, MATRIX_1:def 8 ; :: thesis: verum

end;

A20: len (Col ((QuadraticForm (x,M,y)),i)) = len x by A3, MATRIX_1:def 8;
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 A20, RVSUM_1:117;
then A21: (y . i) * (mlt (x,(Col (M,i)))) = Col ((QuadraticForm (x,M,y)),i) by A13, FINSEQ_1:14;
(mlt ((x * M),y)) . i = ((x * M) . i) * (y . i) by RVSUM_1:59
.= (x "*" (Col (M,i))) * (y . i) by A1, A10, Th40
.= Sum ((y . i) * (mlt (x,(Col (M,i))))) by RVSUM_1:87 ;
hence (ColSum (QuadraticForm (x,M,y))) . i = (mlt ((x * M),y)) . i by A4, A8, A21, Def2; :: thesis: verum

end;

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