let G, H be 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 bijective ; :: thesis: h " is Homomorphism of H,G
then A2: ( h is one-to-one & rng h = the carrier of H ) by FUNCT_2:def 3;
then reconsider h1 = h " as Function of H,G by FUNCT_2:25;

now :: thesis: for a, b being Element of H holds h1 . (a * b) = (h1 . a) * (h1 . b)

let a, b be Element of H; :: thesis: h1 . (a * b) = (h1 . a) * (h1 . b)
set a1 = h1 . a;
set b1 = h1 . b;
( h . (h1 . a) = a & h . (h1 . b) = b ) by A2, FUNCT_1:32;
hence h1 . (a * b) = h1 . (h . ((h1 . a) * (h1 . b))) by Def6
.= (h1 . a) * (h1 . b) by A1, FUNCT_2:26 ;
:: thesis: verum

end;

hence h " is Homomorphism of H,G by Def6; :: thesis: verum