let f be Function of X,Y; :: thesis: f is Function-yielding
let x be set ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 f or f . x is set )
assume x in dom f ; :: thesis: f . x is set
then ( f . x in rng f & rng f c= Y ) by FUNCT_1:def 5;
then f . x is Element of Y ;
hence f . x is set ; :: thesis: verum