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