:: deftheorem defines FinSeq LIOUVIL1:def 2 :
for f being Real_Sequence
for n being Nat holds FinSeq (f,n) = f | (Seg n);