theorem :: GROUP_6:61

for G being set
for H being non empty set
for h being Function of G,H st h is bijective holds
( dom h = G & rng h = H ) by FUNCT_2:def 1, FUNCT_2:def 3;