:: deftheorem Def5 defines (1). GROUP_23:def 4 :
for I being non empty set
for F being Group-Family of I
for b₃ being componentwise_strict Subgroup-Family of F holds
( b₃ = (1). F iff for i being Element of I holds b₃ . i = (1). (F . i) );