theorem :: FINSEQ_6:25

for f being FinSequence holds Rev (Rev f) = f ;