theorem Th19: :: LIOUVIL1:19

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