let F be Function; :: thesis: ( F is empty implies F is FinSequence-yielding )
assume A1: F is empty ; :: 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 )
thus ( x in dom F implies F . x is FinSequence ) by A1; :: thesis: verum