let f be FinSequence; :: thesis: ( len f = 1 implies Rev f = f )
assume len f = 1 ; :: thesis: Rev f = f
then f = <*(f . 1)*> by FINSEQ_1:40;
hence Rev f = f by FINSEQ_5:60; :: thesis: verum