theorem Th51: :: GROUP_19:51

for I being non empty set
for G being Group
for a being finite-support Function of I,G
for W being finite Subset of I st support a c= W & ( for i, j being Element of I holds (a . i) * (a . j) = (a . j) * (a . i) ) holds
Product a = Product (a | W)