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) )

(a * (A @)) * (i,j) = (a * A) * (j,i)

hence (a * A) @ = a * (A @) by A1, A2, A3, MATRIX_0:def 6; :: thesis: verum

(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

A3:
for i, j being Nat st [j,i] in Indices (a * A) holds
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;( 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

(a * (A @)) * (i,j) = (a * A) * (j,i)

proof

( len (a * (A @)) = len (A @) & width A = width (a * A) )
by Th27;
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;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

hence (a * A) @ = a * (A @) by A1, A2, A3, MATRIX_0:def 6; :: thesis: verum