let G, H be set ; :: thesis: 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
let g be Function of G,H; :: thesis: for h being Function of H,G st h * g = id G & g * h = id H holds
h is bijective
let h be Function of H,G; :: thesis: ( h * g = id G & g * h = id H implies h is bijective )
assume ( h * g = id G & g * h = id H ) ; :: thesis: h is bijective
then ( h is one-to-one & h is onto ) by FUNCT_2:23;
hence h is bijective ; :: thesis: verum