:: deftheorem Def7 defines sum_bundle GROUP_21:def 7 :
for I being non empty set
for J being ManySortedSet of I
for F being Group-Family of I,J
for b₄ being Group-Family of I holds
( b₄ = sum_bundle F iff for i being Element of I holds b₄ . i = sum (F . i) );