theorem :: CARDFIL3:39

for I being non empty set
for L being Abelian TopaddGroup
for x being the carrier of b₂ -valued ManySortedSet of I
for J, e being Element of Fin I st e = {} holds
( Sum (x,e) = 0_ L & ( for e, f being Element of Fin I st e misses f holds
Sum (x,(e \/ f)) = (Sum (x,e)) + (Sum (x,f)) ) )