consider f being FinSequence, I being set ;
take F = I --> f; :: thesis: F is FinSequence-yielding
let x be set ; :: according to PRE_POLY:def 3 :: thesis: ( x in dom F implies F . x is FinSequence )
assume A1: x in dom F ; :: thesis: F . x is FinSequence
hence F . x is FinSequence by FUNCOP_1:13; :: thesis: verum