let f be Relation; :: thesis: ( f is complex-valued implies f is COMPLEX -valued )
assume f is complex-valued ; :: thesis: f is COMPLEX -valued
hence rng f c= COMPLEX by VALUED_0:def 1; :: according to RELAT_1:def 19 :: thesis: verum