theorem Th34: :: DIFF_3:34

for h, x being Real
for f1, f2 being Function of REAL,REAL holds ((cdif ((f1 (#) f2),h)) . 1) . x = ((f1 . (x + (h / 2))) * (((cdif (f2,h)) . 1) . x)) + ((f2 . (x - (h / 2))) * (((cdif (f1,h)) . 1) . x))