theorem Th3: :: POLYNOM3:3

for p being FinSequence of REAL holds Sum p = Sum (Rev p)