theorem Th2: :: NOMIN_1:2

for n being Nat
for f being Function st dom f = NAT holds
f | (Seg n) is FinSequence