:: deftheorem defines component-commutative GROUP_20:def 2 :
for I being set
for G being Group
for F being Subgroup-Family of I,G holds
( F is component-commutative iff for i, j being object
for gi, gj being Element of G st i in I & j in I & i <> j holds
ex Fi, Fj being Subgroup of G st
( Fi = F . i & Fj = F . j & ( gi in Fi & gj in Fj implies gi * gj = gj * gi ) ) );