:: deftheorem Def7 defines * MATRIXR1:def 7 :
for a being Real
for A, b₃ being Matrix of REAL holds
( b₃ = a * A iff for ea being Element of F_Real st ea = a holds
b₃ = MXF2MXR (ea * (MXR2MXF A)) );