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 (b * A) = len A & width (b * A) = width A ) by Th5;
A2: ( len ((a * b) * A) = len A & width ((a * b) * A) = width A ) by Th5;
A3: len (a * (b * A)) = len (b * A) by Th5;
then A4: len (a * (b * A)) = len A by Th5;
A5: width (a * (b * A)) = width (b * A) by Th5;
then A6: width (a * (b * A)) = width A by Th5;
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 (a * (b * A)) = Indices (b * A) by A3, A5, MATRIX_4:55;
A9: Indices (b * A) = Indices A by A1, MATRIX_4:55;
reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def 13;
(a * (b * A)) * i,j = a * ((b * A) * i0,j0) by A3, A5, A7, A8, Th3
.= a * (b * (A * i0,j0)) by A3, A4, A5, A6, A7, A8, A9, Th3
.= (a * b) * (A * i0,j0)
.= ((a * b) * A) * i,j by A2, A7, A8, A9, Th3 ;
hence (a * (b * A)) * i,j = ((a * b) * A) * i,j ; :: thesis: verum

end;

hence (a * b) * A = a * (b * A) by A2, A4, A6, MATRIX_1:21; :: thesis: verum