:: deftheorem defines Product GROUP_19:def 4 :
for I being set
for G being Group
for a being finite-support Function of I,G holds Product a = Product (a | (support a));