let x, y be FinSequence of REAL ; :: thesis: for M being Matrix of REAL st len y = len M & len x = width M & len x > 0 & len y > 0 holds
|((M * x),y)| = |(x,((M @) * y))|
let M be Matrix of REAL; :: thesis: ( len y = len M & len x = width M & len x > 0 & len y > 0 implies |((M * x),y)| = |(x,((M @) * y))| )
assume that
A1: len y = len M and
A2: len x = width M and
A3: len x > 0 and
A4: len y > 0 ; :: thesis: |((M * x),y)| = |(x,((M @) * y))|
A5: ( len (M @) = width M & width (M @) = len M ) by A2, A3, MATRIX_0:54;
thus |((M * x),y)| = |((x * (M @)),y)| by A1, A2, A3, A4, MATRIXR1:53
.= |(x,((M @) * y))| by A1, A2, A4, A5, Th47 ; :: thesis: verum