theorem :: FINSEQ_9:18

for f being real-valued Function holds f is Function of (dom f),REAL