for G, H being set
for g being Function of G,H
for h being Function of H,G st h * g = id G & g * h = id H holds
h is bijective by FUNCT_2:23;