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