theorem :: FINSEQ_9:7

for f being Relation holds
( f is REAL -valued iff rng f is real-membered )