theorem Th4: :: TOPREAL7:4

for i being Nat
for f, g being FinSequence st len f < i & i <= (len f) + (len g) holds
i - (len f) in dom g