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:70;
then A3: h2 is onto by FUNCT_2:def 3;
rng h1 = the carrier of H1 by A1, GROUP_6:70;
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:70;
then Gr2Iso h1,h2 is one-to-one by Th3;
hence Gr2Iso h1,h2 is bijective by A4, GROUP_6:70; :: thesis: verum