theorem :: RELSET_3:51

for z1, z2 being Complex holds (multRel (COMPLEX,z1)) * (multRel (COMPLEX,z2)) = multRel (COMPLEX,(z1 * z2))