theorem :: GROUP_1A:241

for G being addGroup
for a, b, c, d being Element of G holds {a,b} * {c,d} = {(a * c),(a * d),(b * c),(b * d)}