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