let x, y be FinSequence of COMPLEX ; :: thesis: for M being Matrix of COMPLEX st len x = width M & len y = len M & len x > 0 & len y > 0 holds
|(x,((M @") * y))| = SumAll (QuadraticForm (x,(M @),y))
let M be Matrix of COMPLEX; :: thesis: ( len x = width M & len y = len M & len x > 0 & len y > 0 implies |(x,((M @") * y))| = SumAll (QuadraticForm (x,(M @),y)) )
assume that
A1: len x = width M and
A2: len y = len M and
A3: len x > 0 and
A4: len y > 0 ; :: thesis: |(x,((M @") * y))| = SumAll (QuadraticForm (x,(M @),y))
A5: width (M @) = len y by A1, A2, A3, MATRIX_0:54;
then A6: width ((M @) *') = len y by Def1;
A7: dom (LineSum (QuadraticForm (x,(M @),y))) = Seg (len (LineSum (QuadraticForm (x,(M @),y)))) by FINSEQ_1:def 3
.= Seg (len (QuadraticForm (x,(M @),y))) by Def9 ;
A8: len (M @) = len x by A1, MATRIX_0:def 6;
A9: len (LineSum (QuadraticForm (x,(M @),y))) = len (QuadraticForm (x,(M @),y)) by Def9
.= len x by A8, A5, Def12 ;
A10: len (M @") = len (M @) by Def1
.= len x by A1, MATRIX_0:def 6 ;
then A11: len ((M @") * y) = len x by Def6;
then len (((M @") * y) *') = len x by COMPLSP2:def 1;
then A12: len (LineSum (QuadraticForm (x,(M @),y))) = len (mlt (x,(((M @") * y) *'))) by A9, FINSEQ_2:72;
A13: 0 + 1 <= len y by A4, NAT_1:13;
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
A14: 1 <= i and
A15: i <= len (LineSum (QuadraticForm (x,(M @),y))) ; :: thesis: (LineSum (QuadraticForm (x,(M @),y))) . i = (mlt (x,(((M @") * y) *'))) . i
A16: len y = width (QuadraticForm (x,(M @),y)) by A8, A5, Def12
.= len (Line ((QuadraticForm (x,(M @),y)),i)) by MATRIX_0:def 7 ;
A17: len (Line ((M @"),i)) = len y by A6, MATRIX_0:def 7;
then A18: len (mlt ((Line ((M @"),i)),y)) >= 1 by A13, FINSEQ_2:72;
len (M @) = len (QuadraticForm (x,(M @),y)) by A8, A5, Def12;
then A19: len (M @) = len (LineSum (QuadraticForm (x,(M @),y))) by Def9;
then A20: i in Seg (len (M @")) by A8, A10, A14, A15, FINSEQ_1:1;
A21: 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

A22: len (Line ((M @),i)) = width (M @) by MATRIX_0:def 7
.= len y by A1, A2, A3, MATRIX_0:54
.= len (y *') by COMPLSP2:def 1 ;
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
A23: 1 <= j and
A24: j <= len (Line ((QuadraticForm (x,(M @),y)),i)) ; :: thesis: ((x . i) * ((mlt ((Line ((M @"),i)),y)) *')) . j = (Line ((QuadraticForm (x,(M @),y)),i)) . j
A25: j in Seg (width (M @)) by A5, A16, A23, A24, FINSEQ_1:1;
j in Seg (len y) by A16, A23, A24, FINSEQ_1:1;
then j in Seg (len (y *')) by COMPLSP2:def 1;
then j in Seg (len (mlt ((Line ((M @),i)),(y *')))) by A22, FINSEQ_2:72;
then A26: j in dom (mlt ((Line ((M @),i)),(y *'))) by FINSEQ_1:def 3;
j in Seg (len (Line ((QuadraticForm (x,(M @),y)),i))) by A23, A24, FINSEQ_1:1;
then A27: j in Seg (width (QuadraticForm (x,(M @),y))) by MATRIX_0:def 7;
j <= width (M @) by A1, A2, A3, A16, A24, MATRIX_0:54;
then A28: [i,j] in Indices (M @) by A14, A15, A19, A23, Th1;
((x . i) * ((mlt ((Line ((M @"),i)),y)) *')) . j = (x . i) * (((mlt ((Line ((M @"),i)),y)) *') . j) by COMPLSP2:16
.= (x . i) * ((mlt (((Line ((M @"),i)) *'),(y *'))) . j) by A17, Th25
.= (x . i) * ((mlt ((Line ((M @),i)),(y *'))) . j) by A8, A10, A20, Th39
.= (x . i) * (((Line ((M @),i)) . j) * ((y *') . j)) by A26, Th17
.= (x . i) * (((Line ((M @),i)) . j) * ((y . j) *')) by A16, A23, A24, COMPLSP2:def 1
.= ((x . i) * ((Line ((M @),i)) . j)) * ((y . j) *')
.= ((x . i) * ((M @) * (i,j))) * ((y . j) *') by A25, MATRIX_0:def 7
.= (QuadraticForm (x,(M @),y)) * (i,j) by A8, A5, A28, Def12 ;
hence ((x . i) * ((mlt ((Line ((M @"),i)),y)) *')) . j = (Line ((QuadraticForm (x,(M @),y)),i)) . j by A27, MATRIX_0:def 7; :: thesis: verum

end;

i in Seg (len (LineSum (QuadraticForm (x,(M @),y)))) by A14, A15, FINSEQ_1:1;
then A29: i in dom (LineSum (QuadraticForm (x,(M @),y))) by FINSEQ_1:def 3;
A30: len (Line ((M @"),i)) = len y by A6, MATRIX_0:def 7;
A31: len ((x . i) * ((mlt ((Line ((M @"),i)),y)) *')) = len ((mlt ((Line ((M @"),i)),y)) *') by COMPLSP2:3
.= len (mlt ((Line ((M @"),i)),y)) by COMPLSP2:def 1
.= len (Line ((QuadraticForm (x,(M @),y)),i)) by A16, A30, FINSEQ_2:72 ;
i in Seg (len (mlt (x,(((M @") * y) *')))) by A12, A14, A15, FINSEQ_1:1;
then i in dom (mlt (x,(((M @") * y) *'))) by FINSEQ_1:def 3;
then (mlt (x,(((M @") * y) *'))) . i = (x . i) * ((((M @") * y) *') . i) by Th17
.= (x . i) * ((((M @") * y) . i) *') by A11, A9, A14, A15, COMPLSP2:def 1 ;
then (mlt (x,(((M @") * y) *'))) . i = (x . i) * ((Sum (mlt ((Line ((M @"),i)),y))) *') by A20, Def6
.= (x . i) * (Sum ((mlt ((Line ((M @"),i)),y)) *')) by A18, Th21
.= Sum ((x . i) * ((mlt ((Line ((M @"),i)),y)) *')) by Th26 ;
then (mlt (x,(((M @") * y) *'))) . i = Sum (Line ((QuadraticForm (x,(M @),y)),i)) by A31, A21, FINSEQ_1:14;
hence (LineSum (QuadraticForm (x,(M @),y))) . i = (mlt (x,(((M @") * y) *'))) . i by A7, A29, Def9; :: thesis: verum

end;

then Sum (LineSum (QuadraticForm (x,(M @),y))) = Sum (mlt (x,(((M @") * y) *'))) by A12, FINSEQ_1:14;
hence |(x,((M @") * y))| = SumAll (QuadraticForm (x,(M @),y)) by A11, Th37; :: thesis: verum