theorem RV: :: FINSEQ_9:6

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