for n, m being Element of NAT
for h, x being Real
for f being Function of REAL,REAL holds ((cdif (((cdif (f,h)) . m),h)) . n) . x = ((cdif (f,h)) . (m + n)) . x