theorem Th10: :: GROUP_20:10

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
for y being finite-support Function of I,(gr UF)
for i being Element of I
for g being Element of (gr UF) st y in product F & y . i = 1_ (F . i) & g in F . i holds
(Product y) * g = g * (Product y)