:: deftheorem defines almost-one-to-one JORDAN23:def 1 :
for f being FinSequence holds
( f is almost-one-to-one iff for i, j being Nat st i in dom f & j in dom f & ( i <> 1 or j <> len f ) & ( i <> len f or j <> 1 ) & f . i = f . j holds
i = j );