theorem :: GROUP_7:32

for G1, G2 being non empty Group-like multMagma holds 1_ (product <*G1,G2*>) = <*(1_ G1),(1_ G2)*>