let x, y be FinSequence of REAL ; for M being Matrix of REAL st len x = len M & len y = width M & len y > 0 holds
|((x * M),y)| = |(x,(M * y))|
let M be Matrix of REAL; ( len x = len M & len y = width M & len y > 0 implies |((x * M),y)| = |(x,(M * y))| )
assume that
A1:
( len x = len M & len y = width M )
and
A2:
len y > 0
; |((x * M),y)| = |(x,(M * y))|
thus |((x * M),y)| =
SumAll (QuadraticForm (x,M,y))
by A1, Th46
.=
|(x,(M * y))|
by A1, A2, Th44
; verum