theorem :: FILEREC1:17

for f being FinSequence st len f = 0 holds
Rev f = f