let f be Function; :: thesis: ( f is nonpair-yielding implies rng f is without_pairs )

assume A1: for x being set st x in dom f holds

not f . x is pair ; :: according to FACIRC_1:def 3 :: thesis: rng f is without_pairs

let y be pair object ; :: according to FACIRC_1:def 2 :: thesis: not y in rng f

assume y in rng f ; :: thesis: contradiction

then ex x being object st

( x in dom f & y = f . x ) by FUNCT_1:def 3;

hence contradiction by A1; :: thesis: verum

assume A1: for x being set st x in dom f holds

not f . x is pair ; :: according to FACIRC_1:def 3 :: thesis: rng f is without_pairs

let y be pair object ; :: according to FACIRC_1:def 2 :: thesis: not y in rng f

assume y in rng f ; :: thesis: contradiction

then ex x being object st

( x in dom f & y = f . x ) by FUNCT_1:def 3;

hence contradiction by A1; :: thesis: verum