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

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