let x, y be FinSequence of COMPLEX ; :: thesis: for M being Matrix of COMPLEX st len x = width M & len y = len M & width M > 0 & len M > 0 holds
|((M * x),y)| = |(x,((M @") * y))|
let M be Matrix of COMPLEX; :: thesis: ( len x = width M & len y = len M & width M > 0 & len M > 0 implies |((M * x),y)| = |(x,((M @") * y))| )
assume that
A1: len x = width M and
A2: len y = len M and
A3: width M > 0 and
A4: len M > 0 ; :: thesis: |((M * x),y)| = |(x,((M @") * y))|
|(x,((M @") * y))| = SumAll (QuadraticForm (x,(M @),y)) by A1, A2, A3, A4, Th55;
hence |((M * x),y)| = |(x,((M @") * y))| by A1, A2, A3, A4, Th56; :: thesis: verum