let f be Function; :: thesis: ( f is Y -valued implies f is Function-yielding )
assume A1: f is Y -valued ; :: 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 A1; :: thesis: verum