theorem Th5: :: POLYNOM1:5

for L being non empty addLoopStr
for F, G being FinSequence of the carrier of L * holds Sum (F ^ G) = (Sum F) ^ (Sum G)