thus F . e is FinSequence of (TOP-REAL 2) by FINSEQ_2:def 3; :: thesis: verum