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)

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)