theorem :: FINSEQ_3:117

for t being FinSequence of INT holds t is FinSequence of REAL