:: deftheorem Def7 defines * MATRIX_5:def 7 :
for x being Complex
for A, b₃ being Matrix of COMPLEX holds
( b₃ = x * A iff for ea being Element of F_Complex st ea = x holds
b₃ = Field2COMPLEX (ea * (COMPLEX2Field A)) );