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

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