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, Th60;
hence |((M * x),y)| = |(x,((M @" ) * y))| by A1, A2, A3, A4, Th61; :: thesis: verum