let G, H be AddGroup; :: 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;

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)

hence
h " is Homomorphism of H,G
by VECTSP_1:def 20; :: thesis: verumlet 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 VECTSP_1:def 20

.= (h1 . a) + (h1 . b) by A1, FUNCT_2:26 ;

:: thesis: verum

end;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 VECTSP_1:def 20

.= (h1 . a) + (h1 . b) by A1, FUNCT_2:26 ;

:: thesis: verum