let h, x be 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))
let f1, f2 be Function of REAL,REAL; ((cdif ((f1 (#) f2),h)) . 1) . x = ((f1 . (x + (h / 2))) * (((cdif (f2,h)) . 1) . x)) + ((f2 . (x - (h / 2))) * (((cdif (f1,h)) . 1) . x))
((cdif ((f1 (#) f2),h)) . 1) . x =
((cdif ((f1 (#) f2),h)) . (0 + 1)) . x
.=
(cD (((cdif ((f1 (#) f2),h)) . 0),h)) . x
by DIFF_1:def 8
.=
(cD ((f1 (#) f2),h)) . x
by DIFF_1:def 8
.=
((f1 (#) f2) . (x + (h / 2))) - ((f1 (#) f2) . (x - (h / 2)))
by DIFF_1:5
.=
((f1 . (x + (h / 2))) * (f2 . (x + (h / 2)))) - ((f1 (#) f2) . (x - (h / 2)))
by VALUED_1:5
.=
((f1 . (x + (h / 2))) * (f2 . (x + (h / 2)))) - ((f1 . (x - (h / 2))) * (f2 . (x - (h / 2))))
by VALUED_1:5
.=
((f1 . (x + (h / 2))) * ((f2 . (x + (h / 2))) - (f2 . (x - (h / 2))))) + ((f2 . (x - (h / 2))) * ((f1 . (x + (h / 2))) - (f1 . (x - (h / 2)))))
.=
((f1 . (x + (h / 2))) * ((cD (f2,h)) . x)) + ((f2 . (x - (h / 2))) * ((f1 . (x + (h / 2))) - (f1 . (x - (h / 2)))))
by DIFF_1:5
.=
((f1 . (x + (h / 2))) * ((cD (f2,h)) . x)) + ((f2 . (x - (h / 2))) * ((cD (f1,h)) . x))
by DIFF_1:5
.=
((f1 . (x + (h / 2))) * ((cD (((cdif (f2,h)) . 0),h)) . x)) + ((f2 . (x - (h / 2))) * ((cD (f1,h)) . x))
by DIFF_1:def 8
.=
((f1 . (x + (h / 2))) * ((cD (((cdif (f2,h)) . 0),h)) . x)) + ((f2 . (x - (h / 2))) * ((cD (((cdif (f1,h)) . 0),h)) . x))
by DIFF_1:def 8
.=
((f1 . (x + (h / 2))) * (((cdif (f2,h)) . (0 + 1)) . x)) + ((f2 . (x - (h / 2))) * ((cD (((cdif (f1,h)) . 0),h)) . x))
by DIFF_1:def 8
.=
((f1 . (x + (h / 2))) * (((cdif (f2,h)) . 1) . x)) + ((f2 . (x - (h / 2))) * (((cdif (f1,h)) . 1) . x))
by DIFF_1:def 8
;
hence
((cdif ((f1 (#) f2),h)) . 1) . x = ((f1 . (x + (h / 2))) * (((cdif (f2,h)) . 1) . x)) + ((f2 . (x - (h / 2))) * (((cdif (f1,h)) . 1) . x))
; verum