let G1, G2, H1, H2 be Group; :: thesis: for f being Homomorphism of G1,H1
for g being Homomorphism of G2,H2 st f is bijective & g is bijective holds
Gr2Iso (f,g) is bijective
let h1 be Homomorphism of G1,H1; :: thesis: for g being Homomorphism of G2,H2 st h1 is bijective & g is bijective holds
Gr2Iso (h1,g) is bijective
let h2 be Homomorphism of G2,H2; :: thesis: ( h1 is bijective & h2 is bijective implies Gr2Iso (h1,h2) is bijective )
assume that
A1: h1 is bijective and
A2: h2 is bijective ; :: thesis: Gr2Iso (h1,h2) is bijective
set h = Gr2Iso (h1,h2);
rng h2 = the carrier of H2 by A2, GROUP_6:60;
then A3: h2 is onto by FUNCT_2:def 3;
rng h1 = the carrier of H1 by A1, GROUP_6:60;
then h1 is onto by FUNCT_2:def 3;
then Gr2Iso (h1,h2) is onto by A3, Th4;
then A4: rng (Gr2Iso (h1,h2)) = the carrier of (product <*H1,H2*>) by FUNCT_2:def 3;
( h1 is one-to-one & h2 is one-to-one ) by A1, A2, GROUP_6:60;
then Gr2Iso (h1,h2) is one-to-one by Th3;
hence Gr2Iso (h1,h2) is bijective by A4, GROUP_6:60; :: thesis: verum