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_0:54;
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