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