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_0:54;
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_0:def 6; :: 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_0:def 6;
then (a * (A @)) * (i,j) = a * ((A @) * (i,j)) by Th29;
then (a * (A @)) * (i,j) = a * (A * (j,i)) by A4, MATRIX_0:def 6
.= (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_0:def 6; :: thesis: verum