theorem :: GROUP_12:7

for I being non empty set
for F being Group-like associative multMagma-Family of I
for i, j being Element of I
for x, y being Element of (product F) st i <> j & x in ProjGroup (F,i) & y in ProjGroup (F,j) holds
x * y = y * x