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