let x, y be FinSequence of REAL ; :: thesis: for M being Matrix of REAL st len x = len M & len y = width M & len y > 0 holds
|(x,(M * y))| = SumAll (QuadraticForm (x,M,y))
let M be Matrix of REAL; :: thesis: ( len x = len M & len y = width M & len y > 0 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 and
A3: len y > 0 ; :: thesis: |(x,(M * y))| = SumAll (QuadraticForm (x,M,y))
A4: width (QuadraticForm (x,M,y)) = len y by A1, A2, Def4;
A5: len (LineSum (QuadraticForm (x,M,y))) = len (QuadraticForm (x,M,y)) by Th20;
len (M * y) = len x by A1, A2, A3, MATRIXR1:61;
then A6: len (mlt (x,(M * y))) = len x by Th30
.= len (LineSum (QuadraticForm (x,M,y))) by A1, A2, A5, Def4 ;
for i being Nat st 1 <= i & i <= len (LineSum (QuadraticForm (x,M,y))) holds
(LineSum (QuadraticForm (x,M,y))) . i = (mlt (x,(M * y))) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (LineSum (QuadraticForm (x,M,y))) implies (LineSum (QuadraticForm (x,M,y))) . i = (mlt (x,(M * y))) . i )
assume that
A7: 1 <= i and
A8: i <= len (LineSum (QuadraticForm (x,M,y))) ; :: thesis: (LineSum (QuadraticForm (x,M,y))) . i = (mlt (x,(M * y))) . i
A9: i in Seg (len (LineSum (QuadraticForm (x,M,y)))) by A7, A8, FINSEQ_1:1;
then A10: i in Seg (len M) by A1, A2, A5, Def4;
then A11: i in Seg (len (M * y)) by A2, A3, MATRIXR1:61;
A12: len (Line (M,i)) = len y by A2, MATRIX_1:def 7;
A13: i <= len M by A10, FINSEQ_1:1;
A14: for j being Nat st 1 <= j & j <= len (Line ((QuadraticForm (x,M,y)),i)) holds
((x . i) * (mlt ((Line (M,i)),y))) . j = (Line ((QuadraticForm (x,M,y)),i)) . j

proof

let j be Nat; :: thesis: ( 1 <= j & j <= len (Line ((QuadraticForm (x,M,y)),i)) implies ((x . i) * (mlt ((Line (M,i)),y))) . j = (Line ((QuadraticForm (x,M,y)),i)) . j )
assume that
A15: 1 <= j and
A16: j <= len (Line ((QuadraticForm (x,M,y)),i)) ; :: thesis: ((x . i) * (mlt ((Line (M,i)),y))) . j = (Line ((QuadraticForm (x,M,y)),i)) . j
j <= width M by A2, A4, A16, MATRIX_1:def 7;
then A17: [i,j] in Indices M by A7, A13, A15, MATRIXC1:1;
j in Seg (len (Line ((QuadraticForm (x,M,y)),i))) by A15, A16, FINSEQ_1:1;
then A18: j in Seg (width (QuadraticForm (x,M,y))) by MATRIX_1:def 7;
thus ((x . i) * (mlt ((Line (M,i)),y))) . j = (x . i) * ((mlt ((Line (M,i)),y)) . j) by RVSUM_1:44
.= (x . i) * (((Line (M,i)) . j) * (y . j)) by RVSUM_1:59
.= (x . i) * ((M * (i,j)) * (y . j)) by A2, A4, A18, MATRIX_1:def 7
.= ((x . i) * (M * (i,j))) * (y . j)
.= (QuadraticForm (x,M,y)) * (i,j) by A1, A2, A17, Def4
.= (Line ((QuadraticForm (x,M,y)),i)) . j by A18, MATRIX_1:def 7 ; :: thesis: verum

end;

A19: len (Line ((QuadraticForm (x,M,y)),i)) = len y by A4, MATRIX_1:def 7;
len (mlt ((Line (M,i)),y)) = len y by A12, Th30;
then len ((x . i) * (mlt ((Line (M,i)),y))) = len (Line ((QuadraticForm (x,M,y)),i)) by A19, RVSUM_1:117;
then A20: (x . i) * (mlt ((Line (M,i)),y)) = Line ((QuadraticForm (x,M,y)),i) by A14, FINSEQ_1:14;
(mlt (x,(M * y))) . i = (x . i) * ((M * y) . i) by RVSUM_1:59
.= (x . i) * ((Line (M,i)) "*" y) by A2, A3, A11, Th41
.= Sum ((x . i) * (mlt ((Line (M,i)),y))) by RVSUM_1:87 ;
hence (LineSum (QuadraticForm (x,M,y))) . i = (mlt (x,(M * y))) . i by A5, A9, A20, Th20; :: thesis: verum

end;

hence |(x,(M * y))| = SumAll (QuadraticForm (x,M,y)) by A6, FINSEQ_1:14; :: thesis: verum