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

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