let n be Nat; :: thesis: for a being Element of F_Real
for A, B being Matrix of n,F_Real st n > 0 holds
(a * A) * B = a * (A * B)
let a be Element of F_Real; :: thesis: for A, B being Matrix of n,F_Real st n > 0 holds
(a * A) * B = a * (A * B)
let A, B be Matrix of n,F_Real; :: thesis: ( n > 0 implies (a * A) * B = a * (A * B) )
assume A1: n > 0 ; :: thesis: (a * A) * B = a * (A * B)
A2: ( width A = n & len A = n & width B = n & len B = n ) by MATRIX_0:24;
reconsider ra = a as Real ;
reconsider rA = A, rB = B as Matrix of n,REAL ;
A3: rA * rB = A * B by ANPROJ_8:17;
a * A = ra * rA by Th46;
then (a * A) * B = (ra * rA) * rB by ANPROJ_8:17
.= ra * (rA * rB) by A2, A1, MATRIXR1:41
.= a * (A * B) by A3, Th46 ;
hence (a * A) * B = a * (A * B) ; :: thesis: verum