theorem :: FINSEQ_9:11

for f being Relation holds
( dom f is integer-membered iff f is INT -defined )