let f be Function; :: thesis: ( f is natural-valued implies f is nonpair-yielding )
assume f is natural-valued ; :: thesis: f is nonpair-yielding
then A1: rng f c= NAT by VALUED_0:def 6;
let x be set ; :: according to FACIRC_1:def 3 :: thesis: ( not x in proj1 f or not f . x is pair )
assume x in dom f ; :: thesis: not f . x is pair
then f . x in rng f by FUNCT_1:def 3;
hence not f . x is pair by A1; :: thesis: verum