theorem :: DIFF_1:27

for n being Nat
for h, x being Real
for f being Function of REAL,REAL holds ((fdif (f,h)) . (2 * n)) . x = ((cdif (f,h)) . (2 * n)) . (x + (n * h))