theorem RestrictedXFin: :: NUMBER06:4

for f being sequence of REAL
for n being Nat holds f | n is XFinSequence