let n be Nat; :: thesis: for a being Real
for M being Matrix of n,REAL
for x being FinSequence of REAL st n > 0 & len x = n holds
M * (a * x) = (a * M) * x
let a be Real; :: thesis: for M being Matrix of n,REAL
for x being FinSequence of REAL st n > 0 & len x = n holds
M * (a * x) = (a * M) * x
let M be Matrix of n,REAL; :: thesis: for x being FinSequence of REAL st n > 0 & len x = n holds
M * (a * x) = (a * M) * x
let x be FinSequence of REAL ; :: thesis: ( n > 0 & len x = n implies M * (a * x) = (a * M) * x )
assume that
A1: n > 0 and
A2: len x = n ; :: thesis: M * (a * x) = (a * M) * x
( width M = n & len M = n ) by MATRIX_0:24;
then A3: ( width M = len (ColVec2Mx x) & len M > 0 & len (ColVec2Mx x) > 0 & width (ColVec2Mx x) > 0 ) by A1, A2, MATRIXR1:def 9;
(a * M) * x = Col (((a * M) * (ColVec2Mx x)),1) by MATRIXR1:def 11
.= Col ((a * (M * (ColVec2Mx x))),1) by A3, MATRIXR1:41
.= Col ((M * (a * (ColVec2Mx x))),1) by A3, MATRIXR1:40
.= Col ((M * (ColVec2Mx (a * x))),1) by A1, A2, MATRIXR1:47
.= M * (a * x) by MATRIXR1:def 11 ;
hence M * (a * x) = (a * M) * x ; :: thesis: verum