:: deftheorem defines is_split_at FINSEQ_6:def 10 :
for F being FinSequence of INT
for n being Nat holds
( F is_split_at n iff for i, j being Nat st 1 <= i & i <= n & n < j & j <= len F holds
F . i <= F . j );