let G, H be Group; :: thesis: for h being Homomorphism of G,H st h * (h " ) = id H & (h " ) * h = id G holds
h is bijective
let h be Homomorphism of G,H; :: thesis: ( h * (h " ) = id H & (h " ) * h = id G implies h is bijective )
assume h * (h " ) = id H ; :: thesis: ( not (h " ) * h = id G or h is bijective )
then A1: rng h = the carrier of H by FUNCT_2:29;
assume (h " ) * h = id G ; :: thesis: h is bijective
then h is one-to-one by WAYBEL_1:25;
hence h is bijective by A1, GROUP_6:70; :: thesis: verum