let f be Function; :: thesis: ( f is ext-real-functions-valued implies f is Function-yielding )

assume A2: f is ext-real-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 A2; :: thesis: verum

assume A2: f is ext-real-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 A2; :: thesis: verum