let f be Function; :: thesis: ( f is FinSequence-yielding implies f is Function-yielding )
assume A1: f is FinSequence-yielding ; :: thesis: f is Function-yielding
let x be set ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 f or f . x is set )
thus ( not x in proj1 f or f . x is set ) by A1, Def3; :: thesis: verum