theorem :: RELSET_3:53

for z being Complex holds multRel (COMPLEX,z) = { [z1,(z1 * z)] where z1 is Complex : verum }