theorem :: DIFF_3:35

for h, x being Real
for f1, f2 being Function of REAL,REAL
for S being Seq_Sequence st ( for n, i being Nat st i <= n holds
(S . n) . i = ((n choose i) * (((cdif (f1,h)) . i) . (x + ((n -' i) * (h / 2))))) * (((cdif (f2,h)) . (n -' i)) . (x - (i * (h / 2)))) ) holds
( ((cdif ((f1 (#) f2),h)) . 1) . x = Sum ((S . 1),1) & ((cdif ((f1 (#) f2),h)) . 2) . x = Sum ((S . 2),2) )