theorem :: FINSEQ_9:14

for f being Relation holds
( dom f is complex-membered iff f is COMPLEX -defined )