let h, x be Real; 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; ((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)))
; verum