let a be Real; :: thesis: for A, B being Matrix of REAL st width A = len B & len A > 0 & len B > 0 & width B > 0 holds
(a * A) * B = a * (A * B)
let A, B be Matrix of REAL ; :: thesis: ( width A = len B & len A > 0 & len B > 0 & width B > 0 implies (a * A) * B = a * (A * B) )
assume that
A1: width A = len B and
A2: len A > 0 and
A3: len B > 0 and
A4: width B > 0 ; :: thesis: (a * A) * B = a * (A * B)
( len (A @ ) = width A & width (B @ ) = len B ) by A1, A3, A4, MATRIX_2:12;
then (B @ ) * (a * (A @ )) = a * ((B @ ) * (A @ )) by A1, Th40;
then A5: (B @ ) * (a * (A @ )) = a * ((A * B) @ ) by A1, A4, MATRIX_3:24;
A6: width (a * (A * B)) = width (A * B) by Th27
.= width B by A1, MATRIX_3:def 4 ;
A7: len (a * (A * B)) = len (A * B) by Th27
.= len A by A1, MATRIX_3:def 4 ;
A8: len (a * A) = len A by Th27;
A9: width (a * A) = width A by Th27;
width (A * B) = width B by A1, MATRIX_3:def 4;
then (B @ ) * (a * (A @ )) = (a * (A * B)) @ by A4, A5, Th30;
then (B @ ) * ((a * A) @ ) = (a * (A * B)) @ by A1, A3, Th30;
then A10: ((a * A) * B) @ = (a * (A * B)) @ by A1, A4, A9, MATRIX_3:24;
( len ((a * A) * B) = len (a * A) & width ((a * A) * B) = width B ) by A1, A9, MATRIX_3:def 4;
then (a * A) * B = ((a * (A * B)) @ ) @ by A2, A4, A8, A10, MATRIX_2:15;
hence (a * A) * B = a * (A * B) by A2, A4, A7, A6, MATRIX_2:15; :: thesis: verum