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