for n being Nat
for r being Real holds (c_d r) . n >= 0