theorem Th29: :: E_TRANS1:29

for F being FinSequence of the carrier of (Polynom-Ring INT.Ring) holds Sum (^ F) = ^ (Sum F)