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)| = |(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)| = |(x,(M * y))| )
assume that
A1: ( len x = len M & len y = width M ) and
A2: len y > 0 ; :: thesis: |((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 ; :: thesis: verum