let a, b be Real; :: thesis: for A being Matrix of REAL holds (a * b) * A = a * (b * A)
let A be Matrix of REAL; :: thesis: (a * b) * A = a * (b * A)
A1: ( len ((a * b) * A) = len A & width ((a * b) * A) = width A ) by Th5;
A2: len (a * (b * A)) = len (b * A) by Th5;
A3: width (a * (b * A)) = width (b * A) by Th5;
then A4: width (a * (b * A)) = width A by Th5;
A5: ( len (b * A) = len A & width (b * A) = width A ) by Th5;
A6: for i, j being Nat st [i,j] in Indices (a * (b * A)) holds
(a * (b * A)) * (i,j) = ((a * b) * A) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (a * (b * A)) implies (a * (b * A)) * (i,j) = ((a * b) * A) * (i,j) )
assume A7: [i,j] in Indices (a * (b * A)) ; :: thesis: (a * (b * A)) * (i,j) = ((a * b) * A) * (i,j)
A8: Indices (b * A) = Indices A by A5, MATRIX_4:55;
reconsider i0 = i, j0 = j as Nat ;
A9: Indices (a * (b * A)) = Indices (b * A) by A2, A3, MATRIX_4:55;
then (a * (b * A)) * (i,j) = a * ((b * A) * (i0,j0)) by A7, Th3
.= a * (b * (A * (i0,j0))) by A7, A9, A8, Th3
.= (a * b) * (A * (i0,j0))
.= ((a * b) * A) * (i,j) by A7, A9, A8, Th3 ;
hence (a * (b * A)) * (i,j) = ((a * b) * A) * (i,j) ; :: thesis: verum

end;

len (a * (b * A)) = len A by A2, Th5;
hence (a * b) * A = a * (b * A) by A1, A4, A6, MATRIX_0:21; :: thesis: verum