theorem :: GROUP_7:29

for G1, G2 being non empty multMagma
for x1, x2 being Element of G1
for y1, y2 being Element of G2 holds <*x1,y1*> * <*x2,y2*> = <*(x1 * x2),(y1 * y2)*>