let G1, G2, H1, H2 be Group; :: thesis: ( G1,H1 are_isomorphic & G2,H2 are_isomorphic implies product <*G1,G2*>, product <*H1,H2*> are_isomorphic )
given h1 being Homomorphism of G1,H1 such that A1: h1 is bijective ; :: according to GROUP_6:def 11 :: thesis: ( not G2,H2 are_isomorphic or product <*G1,G2*>, product <*H1,H2*> are_isomorphic )
given h2 being Homomorphism of G2,H2 such that A2: h2 is bijective ; :: according to GROUP_6:def 11 :: thesis: product <*G1,G2*>, product <*H1,H2*> are_isomorphic
take Gr2Iso (h1,h2) ; :: according to GROUP_6:def 11 :: thesis: Gr2Iso (h1,h2) is bijective
thus Gr2Iso (h1,h2) is bijective by A1, A2, Th5; :: thesis: verum