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 A1: ( width A = len B & len A > 0 & len B > 0 & width B > 0 ) ; :: thesis: (a * A) * B = a * (A * B)
then A2: ( len (A @ ) = width A & width (A @ ) = len A ) by MATRIX_2:12;
A3: width (A * B) = width B by A1, MATRIX_3:def 4;
A4: len (A * B) = len A by A1, MATRIX_3:def 4;
A5: width (a * A) = width A by Th27;
then A6: len ((a * A) * B) = len (a * A) by A1, MATRIX_3:def 4;
A7: width ((a * A) * B) = width B by A1, A5, MATRIX_3:def 4;
A8: len (a * A) = len A by Th27;
A9: len (a * (A * B)) = len (A * B) by Th27
.= len A by A1, MATRIX_3:def 4 ;
A10: width (a * (A * B)) = width (A * B) by Th27
.= width B by A1, MATRIX_3:def 4 ;
( len (B @ ) = width B & width (B @ ) = len B ) by A1, MATRIX_2:12;
then (B @ ) * (a * (A @ )) = a * ((B @ ) * (A @ )) by A1, A2, Th40;
then (B @ ) * (a * (A @ )) = a * ((A * B) @ ) by A1, MATRIX_3:24;
then (B @ ) * (a * (A @ )) = (a * (A * B)) @ by A1, A3, A4, Th30;
then (B @ ) * ((a * A) @ ) = (a * (A * B)) @ by A1, Th30;
then ((a * A) * B) @ = (a * (A * B)) @ by A1, A5, MATRIX_3:24;
then (a * A) * B = ((a * (A * B)) @ ) @ by A1, A6, A7, A8, MATRIX_2:15;
hence (a * A) * B = a * (A * B) by A1, A9, A10, MATRIX_2:15; :: thesis: verum