theorem Th56: :: MATRIXC1:58

for x, y being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len y = len M & len x = width M & len x > 0 & len y > 0 holds
|((M * x),y)| = SumAll (QuadraticForm (x,(M @),y))