let a be Real; :: thesis: for A being Matrix of REAL st width A > 0 holds
(a * A) @ = a * (A @ )
let A be Matrix of REAL ; :: thesis: ( width A > 0 implies (a * A) @ = a * (A @ ) )
assume width A > 0 ; :: thesis: (a * A) @ = a * (A @ )
then A1: len (A @ ) = width A by MATRIX_2:12;
A2: 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) )
( Indices (a * (A @ )) = Indices (A @ ) & Indices (a * A) = Indices A ) by Th28;
hence ( [i,j] in Indices (a * (A @ )) iff [j,i] in Indices (a * A) ) by MATRIX_1:def 7; :: thesis: verum

end;

A3: 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 A4: [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 A4, MATRIX_1:def 7
.= (a * A) * j,i by A4, Th29 ;
hence (a * (A @ )) * i,j = (a * A) * j,i ; :: thesis: verum

end;

( len (a * (A @ )) = len (A @ ) & width A = width (a * A) ) by Th27;
hence (a * A) @ = a * (A @ ) by A1, A2, A3, MATRIX_1:def 7; :: thesis: verum