let a be Real; :: thesis: for A being Matrix of REAL st len A > 0 & width A > 0 holds
(a * A) @ = a * (A @ )
let A be Matrix of REAL ; :: thesis: ( len A > 0 & width A > 0 implies (a * A) @ = a * (A @ ) )
assume A1: ( len A > 0 & width A > 0 ) ; :: thesis: (a * A) @ = a * (A @ )
A2: len (a * (A @ )) = len (A @ ) by Th27;
A3: len (A @ ) = width A by A1, MATRIX_2:12;
A4: width A = width (a * A) by Th27;
A5: for i, j being Nat holds
( [i,j] in Indices (a * (A @ )) iff [j,i] in Indices (a * A) )

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (a * (A @ )) iff [j,i] in Indices (a * A) )
A6: Indices (a * (A @ )) = Indices (A @ ) by Th28;
Indices (a * A) = Indices A by Th28;
hence ( [i,j] in Indices (a * (A @ )) iff [j,i] in Indices (a * A) ) by A6, MATRIX_1:def 7; :: thesis: verum

end;

for i, j being Nat st [j,i] in Indices (a * A) holds
(a * (A @ )) * i,j = (a * A) * j,i

proof

let i, j be Nat; :: thesis: ( [j,i] in Indices (a * A) implies (a * (A @ )) * i,j = (a * A) * j,i )
assume [j,i] in Indices (a * A) ; :: thesis: (a * (A @ )) * i,j = (a * A) * j,i
then A7: [j,i] in Indices A by Th28;
then [i,j] in Indices (A @ ) by MATRIX_1:def 7;
then (a * (A @ )) * i,j = a * ((A @ ) * i,j) by Th29;
then (a * (A @ )) * i,j = a * (A * j,i) by A7, MATRIX_1:def 7
.= (a * A) * j,i by A7, Th29 ;
hence (a * (A @ )) * i,j = (a * A) * j,i ; :: thesis: verum

end;

hence (a * A) @ = a * (A @ ) by A2, A3, A4, A5, MATRIX_1:def 7; :: thesis: verum