theorem :: FINSEQ_5:60
for x being object holds Rev <*x*> = <*x*>