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