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