for f being Real_Sequence
for n being Nat holds dom (FinSeq (f,n)) = Seg n