theorem Th53: :: GROUP_19:53

for I being non empty set
for G being Group
for F being Group-Family of I
for sx, sy being Element of (sum F)
for x, y, xy being finite-support Function of I,G st ( for i being Element of I holds F . i is Subgroup of G ) & ( for i, j being Element of I
for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds
gi * gj = gj * gi ) & sx = x & sy = y & sx * sy = xy holds
Product xy = (Product x) * (Product y)