let f be Relation; :: thesis: ( f is COMPLEX -valued iff rng f is complex-membered )
( f is COMPLEX -valued iff f is complex-valued ) ;
hence ( f is COMPLEX -valued iff rng f is complex-membered ) by CV; :: thesis: verum