let x, y be FinSequence of REAL ; 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; ( 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
; |(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
; verum