let a be Real; :: thesis: for A being Matrix of REAL

for i2, j2 being Nat st [i2,j2] in Indices A holds

(a * A) * (i2,j2) = a * (A * (i2,j2))

let A be Matrix of REAL; :: thesis: for i2, j2 being Nat st [i2,j2] in Indices A holds

(a * A) * (i2,j2) = a * (A * (i2,j2))

let i2, j2 be Nat; :: thesis: ( [i2,j2] in Indices A implies (a * A) * (i2,j2) = a * (A * (i2,j2)) )

reconsider ea = a as Element of F_Real by XREAL_0:def 1;

assume [i2,j2] in Indices A ; :: thesis: (a * A) * (i2,j2) = a * (A * (i2,j2))

then (MXF2MXR (ea * (MXR2MXF A))) * (i2,j2) = ea * ((MXR2MXF A) * (i2,j2)) by MATRIX_3:def 5

.= a * (A * (i2,j2)) ;

hence (a * A) * (i2,j2) = a * (A * (i2,j2)) by Def7; :: thesis: verum

for i2, j2 being Nat st [i2,j2] in Indices A holds

(a * A) * (i2,j2) = a * (A * (i2,j2))

let A be Matrix of REAL; :: thesis: for i2, j2 being Nat st [i2,j2] in Indices A holds

(a * A) * (i2,j2) = a * (A * (i2,j2))

let i2, j2 be Nat; :: thesis: ( [i2,j2] in Indices A implies (a * A) * (i2,j2) = a * (A * (i2,j2)) )

reconsider ea = a as Element of F_Real by XREAL_0:def 1;

assume [i2,j2] in Indices A ; :: thesis: (a * A) * (i2,j2) = a * (A * (i2,j2))

then (MXF2MXR (ea * (MXR2MXF A))) * (i2,j2) = ea * ((MXR2MXF A) * (i2,j2)) by MATRIX_3:def 5

.= a * (A * (i2,j2)) ;

hence (a * A) * (i2,j2) = a * (A * (i2,j2)) by Def7; :: thesis: verum