theorem :: FINSEQ_9:4

for f being Relation holds
( rng f is integer-membered iff f is INT -valued )