theorem TH3: :: ASYMPT_3:25

for f being Function of NAT,REAL st ( for x being Nat holds f . x = 1 / (2 to_power x) ) holds
f is negligible