theorem :: GROUP_7:35

for G1, G2 being Group
for x being Element of G1
for y being Element of G2 holds <*x,y*> " = <*(x "),(y ")*>