let f be Function of A,(Funcs B,C); :: 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 A1: f . x in rng f by FUNCT_1:def 5;
rng f c= Funcs B,C by RELAT_1:def 19;
hence f . x is set by A1; :: thesis: verum