theorem Th9: :: GROUP_20:9

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