for F being FinSequence of REAL holds F is FinSequence of ExtREAL