theorem :: HELLY:1

for p being non empty FinSequence holds <*(p . 1)*> ^' p = p