let f be Relation; :: thesis: ( dom f is complex-membered iff f is COMPLEX -defined )
thus ( dom f is complex-membered implies f is COMPLEX -defined ) :: thesis: ( f is COMPLEX -defined implies dom f is complex-membered )

proof

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

end;

thus ( f is COMPLEX -defined implies dom f is complex-membered ) ; :: thesis: verum