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 by FUNCT_1:def 5;
hence f . x is set ; :: thesis: verum