theorem :: FINSEQ_1:106

for f being real-valued FinSequence holds f is FinSequence of REAL