theorem Th18: :: FINSEQ_5:18

for f being FinSequence
for i being Nat holds dom (f | i) c= dom f