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