theorem Th13: :: NAT_5:13

for f being FinSequence of NAT holds f is FinSequence of REAL