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 15 :: 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 15 :: thesis: product <*G1,G2*>, product <*H1,H2*> are_isomorphic
take h = Gr2Iso h1,h2; :: according to GROUP_6:def 15 :: thesis: h is bijective
thus h is bijective by A1, A2, Th5; :: thesis: verum