:: deftheorem Def2 defines component-commutative GROUP_20:def 3 :
for I being non empty set
for G being Group
for F being Subgroup-Family of I,G holds
( F is component-commutative iff 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 );