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
|(x,(y * M))| = |((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 |(x,(y * M))| = |((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: |(x,(y * M))| = |((x * (M @ )),y)|
A5: ( len (M @ ) = width M & width (M @ ) = len M ) by A2, A3, MATRIX_2:12;
thus |(x,(y * M))| = |(x,((M @ ) * y))| by A1, A2, A3, A4, MATRIXR1:52
.= |((x * (M @ )),y)| by A1, A2, A4, A5, Th47 ; :: thesis: verum