theorem :: FINSEQ_1:108

for f being ext-real-valued FinSequence holds f is FinSequence of ExtREAL