theorem :: GROUP_7:39

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