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_2:12;
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 Def10 ;
A8: len (M @ ) = len x by A1, MATRIX_1:def 7;
A9: len (LineSum (QuadraticForm x,(M @ ),y)) = len (QuadraticForm x,(M @ ),y) by Def10
.= len x by A8, A5, Def13 ;
A10: len (M @" ) = len (M @ ) by Def1
.= len x by A1, MATRIX_1:def 7 ;
then A11: len ((M @" ) * y) = len x by Def7;
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:86;
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, Def13
.= len (Line (QuadraticForm x,(M @ ),y),i) by MATRIX_1:def 8 ;
A17: len (Line (M @" ),i) = len y by A6, MATRIX_1:def 8;
then A18: len (mlt (Line (M @" ),i),y) >= 1 by A13, FINSEQ_2:86;
len (M @ ) = len (QuadraticForm x,(M @ ),y) by A8, A5, Def13;
then A19: len (M @ ) = len (LineSum (QuadraticForm x,(M @ ),y)) by Def10;
then A20: i in Seg (len (M @" )) by A8, A10, A14, A15, FINSEQ_1:3;
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_1:def 8
.= len y by A1, A2, A3, MATRIX_2:12
.= 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:3;
j in Seg (len y) by A16, A23, A24, FINSEQ_1:3;
then j in Seg (len (y *' )) by COMPLSP2:def 1;
then j in Seg (len (mlt (Line (M @ ),i),(y *' ))) by A22, FINSEQ_2:86;
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:3;
then A27: j in Seg (width (QuadraticForm x,(M @ ),y)) by MATRIX_1:def 8;
j <= width (M @ ) by A1, A2, A3, A16, A24, MATRIX_2:12;
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, Th28
.= (x . i) * ((mlt (Line (M @ ),i),(y *' )) . j) by A8, A10, A20, Th43
.= (x . i) * (((Line (M @ ),i) . j) * ((y *' ) . j)) by A26, Th19
.= (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_1:def 8
.= (QuadraticForm x,(M @ ),y) * i,j by A8, A5, A28, Def13 ;
hence ((x . i) * ((mlt (Line (M @" ),i),y) *' )) . j = (Line (QuadraticForm x,(M @ ),y),i) . j by A27, MATRIX_1:def 8; :: thesis: verum

end;

i in Seg (len (LineSum (QuadraticForm x,(M @ ),y))) by A14, A15, FINSEQ_1:3;
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_1:def 8;
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:86 ;
i in Seg (len (mlt x,(((M @" ) * y) *' ))) by A12, A14, A15, FINSEQ_1:3;
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 Th19
.= (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, Def7
.= (x . i) * (Sum ((mlt (Line (M @" ),i),y) *' )) by A18, Th24
.= Sum ((x . i) * ((mlt (Line (M @" ),i),y) *' )) by Th29 ;
then (mlt x,(((M @" ) * y) *' )) . i = Sum (Line (QuadraticForm x,(M @ ),y),i) by A31, A21, FINSEQ_1:18;
hence (LineSum (QuadraticForm x,(M @ ),y)) . i = (mlt x,(((M @" ) * y) *' )) . i by A7, A29, Def10; :: thesis: verum

end;

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