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 st UF = Union (Carrier F) holds
for i being Element of I holds F . i is normal Subgroup of gr UF