theorem Th1: :: FACIRC_1:1

for f being Function st f is nonpair-yielding holds
rng f is without_pairs