theorem Th42: :: RELSET_3:42
for z, z1, z2 being Complex
for X being complex-membered set holds
( [z1,z2] in multRel (X,z) iff ( z1 in X & z2 in X & z2 = z * z1 ) )