theorem :: GROUP_19:31

for I being non empty set
for F being Group-Family of I
for a, b being Element of (product F) st support (a,F) misses support (b,F) holds
a +* (b | (support (b,F))) = a * b