for I being non empty set
for G being Group
for F being component-commutative Subgroup-Family of I,G
for UF being Subset of G st UF = Union (Carrier F) holds
for g being Element of G st g in gr UF holds
ex f being finite-support Function of I,(gr UF) st
( f in sum F & g = Product f )