let f be Function; :: thesis: ( f is complex-functions-valued implies f is Function-yielding )
assume A1: f is complex-functions-valued ; :: thesis: f is Function-yielding
let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in dom f or f . x is set )
thus ( not x in dom f or f . x is set ) by A1; :: thesis: verum