let H, G be Group; :: thesis: for h being Homomorphism of G,H
for g1 being Homomorphism of H,G st h is bijective & g1 = h " holds
g1 is bijective
let h be Homomorphism of G,H; :: thesis: for g1 being Homomorphism of H,G st h is bijective & g1 = h " holds
g1 is bijective
let g1 be Homomorphism of H,G; :: thesis: ( h is bijective & g1 = h " implies g1 is bijective )
assume A1: ( h is bijective & g1 = h " ) ; :: thesis: g1 is bijective
then ( dom h = the carrier of G & rng g1 = dom h ) by FUNCT_1:55, FUNCT_2:def 1;
hence g1 is bijective by A1, Th70; :: thesis: verum