:: deftheorem defines multRel RELSET_3:def 3 :
for X being complex-membered set
for z being Complex holds multRel (X,z) = ((curry multcomplex) . z) |_2 X;