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:3;
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 8;
A13: i <= len M by A10, FINSEQ_1:3;
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 8;
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:3;
then A18: j in Seg (width (QuadraticForm x,M,y)) by MATRIX_1:def 8;
thus ((x . i) * (mlt (Line M,i),y)) . j = (x . i) * ((mlt (Line M,i),y) . j) by RVSUM_1:66
.= (x . i) * (((Line M,i) . j) * (y . j)) by RVSUM_1:86
.= (x . i) * ((M * i,j) * (y . j)) by A2, A4, A18, MATRIX_1:def 8
.= ((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 8 ; :: thesis: verum

end;

A20: len (Line (QuadraticForm x,M,y),i) = len y by A4, MATRIX_1:def 8;
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 A20, RVSUM_1:147;
then A21: (x . i) * (mlt (Line M,i),y) = Line (QuadraticForm x,M,y),i by A14, FINSEQ_1:18;
(mlt x,(M * y)) . i = (x . i) * ((M * y) . i) by RVSUM_1:86
.= (x . i) * ((Line M,i) "*" y) by A2, A3, A11, Th41
.= Sum ((x . i) * (mlt (Line M,i),y)) by RVSUM_1:117 ;
hence (LineSum (QuadraticForm x,M,y)) . i = (mlt x,(M * y)) . i by A5, A9, A21, Th20; :: thesis: verum

end;

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