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