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_0:54;
then (B @) * (a * (A @)) = a * ((B @) * (A @)) by A1, Th40;
then A5: (B @) * (a * (A @)) = a * ((A * B) @) by A1, A4, MATRIX_3:22;
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:22;
( 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_0:57;
hence (a * A) * B = a * (A * B) by A2, A4, A7, A6, MATRIX_0:57; :: thesis: verum