theorem Th5: :: GROUP_12:5

for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for g1, g2 being Element of (product F) st g1 in ProjSet (F,i) & g2 in ProjSet (F,i) holds
g1 * g2 in ProjSet (F,i)