for I being non empty set
for G being Group
for x being finite-support Function of I,G st ( for i being object st i in I holds
x . i = 1_ G ) holds
Product x = 1_ G