let F be Function; :: thesis: ( F is empty implies F is Function-yielding )
assume Z: F is empty ; :: 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 Z; :: thesis: verum