theorem :: RELSET_3:43

for X being complex-membered set st 0 in X holds
multRel (X,0) = [:X,{0}:]