theorem :: RELSET_3:49
for z being Complex
for X being complex-membered set st z <> 0 holds
(multRel (X,z)) ~ = multRel (X,(z "))