theorem :: RELSET_3:18

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