let h, x be Real; for f1, f2 being Function of REAL,REAL holds ((bdif ((f1 (#) f2),h)) . 1) . x = ((f1 . x) * (((bdif (f2,h)) . 1) . x)) + ((f2 . (x - h)) * (((bdif (f1,h)) . 1) . x))
let f1, f2 be Function of REAL,REAL; ((bdif ((f1 (#) f2),h)) . 1) . x = ((f1 . x) * (((bdif (f2,h)) . 1) . x)) + ((f2 . (x - h)) * (((bdif (f1,h)) . 1) . x))
((bdif ((f1 (#) f2),h)) . 1) . x =
((bdif ((f1 (#) f2),h)) . (0 + 1)) . x
.=
(bD (((bdif ((f1 (#) f2),h)) . 0),h)) . x
by DIFF_1:def 7
.=
(bD ((f1 (#) f2),h)) . x
by DIFF_1:def 7
.=
((f1 (#) f2) . x) - ((f1 (#) f2) . (x - h))
by DIFF_1:4
.=
((f1 . x) * (f2 . x)) - ((f1 (#) f2) . (x - h))
by VALUED_1:5
.=
((f1 . x) * (f2 . x)) - ((f1 . (x - h)) * (f2 . (x - h)))
by VALUED_1:5
.=
((f1 . x) * ((f2 . x) - (f2 . (x - h)))) + ((f2 . (x - h)) * ((f1 . x) - (f1 . (x - h))))
.=
((f1 . x) * ((bD (f2,h)) . x)) + ((f2 . (x - h)) * ((f1 . x) - (f1 . (x - h))))
by DIFF_1:4
.=
((f1 . x) * ((bD (f2,h)) . x)) + ((f2 . (x - h)) * ((bD (f1,h)) . x))
by DIFF_1:4
.=
((f1 . x) * ((bD (((bdif (f2,h)) . 0),h)) . x)) + ((f2 . (x - h)) * ((bD (f1,h)) . x))
by DIFF_1:def 7
.=
((f1 . x) * ((bD (((bdif (f2,h)) . 0),h)) . x)) + ((f2 . (x - h)) * ((bD (((bdif (f1,h)) . 0),h)) . x))
by DIFF_1:def 7
.=
((f1 . x) * (((bdif (f2,h)) . (0 + 1)) . x)) + ((f2 . (x - h)) * ((bD (((bdif (f1,h)) . 0),h)) . x))
by DIFF_1:def 7
.=
((f1 . x) * (((bdif (f2,h)) . 1) . x)) + ((f2 . (x - h)) * (((bdif (f1,h)) . 1) . x))
by DIFF_1:def 7
;
hence
((bdif ((f1 (#) f2),h)) . 1) . x = ((f1 . x) * (((bdif (f2,h)) . 1) . x)) + ((f2 . (x - h)) * (((bdif (f1,h)) . 1) . x))
; verum