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 that
A1: h is bijective and
A2: g1 = h " ; :: thesis: g1 is bijective
A3: h is one-to-one by A1;
then A4: g1 is one-to-one by A2;
A5: dom h = the carrier of G by FUNCT_2:def 1;
rng g1 = dom h by A2, A3, FUNCT_1:55;
hence g1 is bijective by A4, A5, Th70; :: thesis: verum