theorem Th3: :: POLYNOM3:3

for p being REAL -valued FinSequence holds Sum p = Sum (Rev p)