theorem :: FINSEQ_9:5

for f being Relation holds
( rng f is rational-membered iff f is RAT -valued )