let a, b be Real; for A being Matrix of REAL holds (a * b) * A = a * (b * A)
let A be Matrix of REAL; (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;
( [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))
;
(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)
;
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; verum