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: ( x in dom f implies f . x is Function )
thus ( x in dom f implies f . x is Function ) by Z; :: thesis: verum