theorem Th7: :: BINOM:7

for R being non empty Abelian add-associative right_zeroed addLoopStr
for p, q being FinSequence of the carrier of R st dom p = dom q holds
Sum (p + q) = (Sum p) + (Sum q)