:: deftheorem Def1A defines circular FINSEQ_6:def 1 :
for D being non empty set
for IT being FinSequence of D holds
( IT is circular iff IT /. 1 = IT /. (len IT) );