theorem :: GROUP_6:60

for G, H being set
for h being Function of G,H holds
( h is bijective iff ( rng h = H & h is one-to-one ) ) by FUNCT_2:def 3;