:: deftheorem Def1 defines complex-valued VALUED_0:def 1 :
for f being Relation holds
( f is complex-valued iff rng f c= COMPLEX );