for G1 being Group holds G1, product <*G1*> are_isomorphic