:: deftheorem Def4 defines Alternating FINSEQ_6:def 7 :
for f being FinSequence holds
( f is Alternating iff for i being Nat st 1 <= i & i + 1 <= len f holds
f . i <> f . (i + 1) );