let f be Relation; :: thesis: ( rng f is complex-membered iff f is complex-valued )
thus ( rng f is complex-membered implies f is complex-valued ) :: thesis: ( f is complex-valued implies rng f is complex-membered )

proof

set E = (rng f) \/ COMPLEX;
reconsider X = rng f as Subset of ((rng f) \/ COMPLEX) by XBOOLE_1:7;
reconsider Y = COMPLEX as Subset of ((rng f) \/ COMPLEX) by XBOOLE_1:7;
assume rng f is complex-membered ; :: thesis: f is complex-valued
then for x being Element of (rng f) \/ COMPLEX st x in rng f holds
x in COMPLEX by XCMPLX_0:def 2;
then X c= Y by SUBSET_1:2;
hence f is complex-valued by VALUED_0:def 1; :: thesis: verum

end;

thus ( f is complex-valued implies rng f is complex-membered ) ; :: thesis: verum