theorem :: FINSEQ_9:13

for f being Relation holds
( dom f is real-membered iff f is REAL -defined )