theorem :: FINSEQ_9:9

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