let D be non empty set ; :: thesis: for f being non empty circular FinSequence of D holds Rev f is circular
let f be non empty circular FinSequence of D; :: thesis: Rev f is circular
thus (Rev f) /. 1 = f /. (len f) by FINSEQ_5:65
.= f /. 1 by Def1A
.= (Rev f) /. (len f) by FINSEQ_5:65
.= (Rev f) /. (len (Rev f)) by FINSEQ_5:def 3 ; :: according to FINSEQ_6:def 1 :: thesis: verum