theorem REV: :: NEWTON04:10

for f being FinSequence holds f = (Rev f) * (Rev (idseq (len f)))