for G1, G2, H1, H2 being Group st G1,H1 are_isomorphic & G2,H2 are_isomorphic holds
product <*G1,G2*>, product <*H1,H2*> are_isomorphic