let a be Element of REAL ; :: thesis: for n being Nat
for M being Matrix of n, REAL holds |:(a * M):| = (abs a) * |:M:|
let n be Nat; :: thesis: for M being Matrix of n, REAL holds |:(a * M):| = (abs a) * |:M:|
let M be Matrix of n, REAL ; :: thesis: |:(a * M):| = (abs a) * |:M:|
A1: ( len (a * M) = len M & width (a * M) = width M & len ((abs a) * |:M:|) = len |:M:| & width ((abs a) * |:M:|) = width |:M:| ) by MATRIXR1:27;
then A2: ( len ((abs a) * |:M:|) = len M & width ((abs a) * |:M:|) = width M ) by Def7;
A3: ( len |:(a * M):| = len (a * M) & width |:(a * M):| = width (a * M) ) by Def7;
for i, j being Nat st [i,j] in Indices |:(a * M):| holds
|:(a * M):| * i,j = ((abs a) * |:M:|) * i,j

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices |:(a * M):| implies |:(a * M):| * i,j = ((abs a) * |:M:|) * i,j )
assume A4: [i,j] in Indices |:(a * M):| ; :: thesis: |:(a * M):| * i,j = ((abs a) * |:M:|) * i,j
A5: Indices |:(a * M):| = Indices (a * M) by Th5;
A6: Indices (a * M) = Indices M by MATRIXR1:28;
A7: |:(a * M):| * i,j = abs ((a * M) * i,j) by A4, A5, Def7
.= abs (a * (M * i,j)) by A1, A4, A5, A6, Th4
.= (abs a) * (abs (M * i,j)) by COMPLEX1:151 ;
A8: ( len ((abs a) * |:M:|) = len |:M:| & width ((abs a) * |:M:|) = width |:M:| ) by MATRIXR1:27;
A9: Indices |:M:| = Indices M by Th5;
A10: Indices (a * M) = Indices M by MATRIXR1:28;
then ((abs a) * |:M:|) * i,j = (abs a) * (|:M:| * i,j) by A4, A5, A8, A9, Th4
.= |:(a * M):| * i,j by A4, A5, A7, A10, Def7 ;
hence |:(a * M):| * i,j = ((abs a) * |:M:|) * i,j ; :: thesis: verum

end;

hence |:(a * M):| = (abs a) * |:M:| by A1, A2, A3, MATRIX_1:21; :: thesis: verum