thus F . e is FinSequence of by FINSEQ_2:def 3; :: thesis: verum