let x be set ; :: according to PRE_POLY:def 3 :: thesis: ( x in dom (i |-> f) implies (i |-> f) . x is FinSequence )
assume x in dom (i |-> f) ; :: thesis: (i |-> f) . x is FinSequence
then x in Seg i by FUNCOP_1:13;
hence (i |-> f) . x is FinSequence by FUNCOP_1:7; :: thesis: verum