let f be PartFunc of A,B; :: 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= B by RELAT_1:def 19;
hence f . x is set by A1; :: thesis: verum