let G be Group; :: thesis: for H being strict Group
for h being Homomorphism of G,H st h is bijective holds
h " is Homomorphism of H,G
let H be strict Group; :: thesis: for h being Homomorphism of G,H st h is bijective holds
h " is Homomorphism of H,G
let h be Homomorphism of G,H; :: thesis: ( h is bijective implies h " is Homomorphism of H,G )
assume A1: ( h is one-to-one & h is onto ) ; :: according to FUNCT_2:def 4 :: thesis: h " is Homomorphism of H,G
then H = Image h by Th67;
hence h " is Homomorphism of H,G by A1, Th65; :: thesis: verum