let h, x be Real; :: thesis: for f1, f2 being Function of REAL , REAL holds ((fdif (f1 (#) f2),h) . 1) . x = ((f1 . x) * (((fdif f2,h) . 1) . x)) + ((((fdif f1,h) . 1) . x) * (f2 . (x + h)))
let f1, f2 be Function of REAL , REAL ; :: thesis: ((fdif (f1 (#) f2),h) . 1) . x = ((f1 . x) * (((fdif f2,h) . 1) . x)) + ((((fdif f1,h) . 1) . x) * (f2 . (x + h)))
((fdif (f1 (#) f2),h) . 1) . x =
((fdif (f1 (#) f2),h) . (0 + 1)) . x
.=
(fD ((fdif (f1 (#) f2),h) . 0 ),h) . x
by Def6
.=
(fD (f1 (#) f2),h) . x
by Def6
.=
((f1 (#) f2) . (x + h)) - ((f1 (#) f2) . x)
by Th3
.=
((f1 . (x + h)) * (f2 . (x + h))) - ((f1 (#) f2) . x)
by VALUED_1:5
.=
((f1 . (x + h)) * (f2 . (x + h))) - ((f1 . x) * (f2 . x))
by VALUED_1:5
.=
((f1 . x) * ((f2 . (x + h)) - (f2 . x))) + (((f1 . (x + h)) - (f1 . x)) * (f2 . (x + h)))
.=
((f1 . x) * ((fD f2,h) . x)) + (((f1 . (x + h)) - (f1 . x)) * (f2 . (x + h)))
by Th3
.=
((f1 . x) * ((fD f2,h) . x)) + (((fD f1,h) . x) * (f2 . (x + h)))
by Th3
.=
((f1 . x) * ((fD ((fdif f2,h) . 0 ),h) . x)) + (((fD f1,h) . x) * (f2 . (x + h)))
by Def6
.=
((f1 . x) * ((fD ((fdif f2,h) . 0 ),h) . x)) + (((fD ((fdif f1,h) . 0 ),h) . x) * (f2 . (x + h)))
by Def6
.=
((f1 . x) * (((fdif f2,h) . (0 + 1)) . x)) + (((fD ((fdif f1,h) . 0 ),h) . x) * (f2 . (x + h)))
by Def6
.=
((f1 . x) * (((fdif f2,h) . 1) . x)) + ((((fdif f1,h) . 1) . x) * (f2 . (x + h)))
by Def6
;
hence
((fdif (f1 (#) f2),h) . 1) . x = ((f1 . x) * (((fdif f2,h) . 1) . x)) + ((((fdif f1,h) . 1) . x) * (f2 . (x + h)))
; :: thesis: verum