let h, x be Real; :: thesis: (fD (((sin (#) cos) (#) cos),h)) . x = (1 / 2) * (((cos (((2 * x) + h) / 2)) * (sin (h / 2))) + ((cos (((6 * x) + (3 * h)) / 2)) * (sin ((3 * h) / 2))))
set y = 3 * x;
set z = 3 * h;
(fD (((sin (#) cos) (#) cos),h)) . x = (((sin (#) cos) (#) cos) . (x + h)) - (((sin (#) cos) (#) cos) . x) by DIFF_1:3
.= (((sin (#) cos) . (x + h)) * (cos . (x + h))) - (((sin (#) cos) (#) cos) . x) by VALUED_1:5
.= (((sin . (x + h)) * (cos . (x + h))) * (cos . (x + h))) - (((sin (#) cos) (#) cos) . x) by VALUED_1:5
.= (((sin . (x + h)) * (cos . (x + h))) * (cos . (x + h))) - (((sin (#) cos) . x) * (cos . x)) by VALUED_1:5
.= (((sin (x + h)) * (cos (x + h))) * (cos (x + h))) - (((sin x) * (cos x)) * (cos x)) by VALUED_1:5
.= ((1 / 4) * ((((sin (((x + h) + (x + h)) - (x + h))) - (sin (((x + h) + (x + h)) - (x + h)))) + (sin (((x + h) + (x + h)) - (x + h)))) + (sin (((x + h) + (x + h)) + (x + h))))) - (((sin x) * (cos x)) * (cos x)) by SIN_COS4:35
.= ((1 / 4) * ((sin (x + h)) + (sin (3 * (x + h))))) - ((1 / 4) * ((((sin ((x + x) - x)) - (sin ((x + x) - x))) + (sin ((x + x) - x))) + (sin ((x + x) + x)))) by SIN_COS4:35
.= ((1 / 4) * ((sin (x + h)) - (sin x))) + ((1 / 4) * ((sin (3 * (x + h))) - (sin (3 * x))))
.= ((1 / 4) * (2 * ((cos (((x + h) + x) / 2)) * (sin (((x + h) - x) / 2))))) + ((1 / 4) * ((sin (3 * (x + h))) - (sin (3 * x)))) by SIN_COS4:16
.= ((1 / 4) * (2 * ((cos (((2 * x) + h) / 2)) * (sin (h / 2))))) + ((1 / 4) * (2 * ((cos ((((3 * x) + (3 * h)) + (3 * x)) / 2)) * (sin ((((3 * x) + (3 * h)) - (3 * x)) / 2))))) by SIN_COS4:16
.= ((1 / 2) * ((cos (((2 * x) + h) / 2)) * (sin (h / 2)))) + ((1 / 2) * ((cos (((6 * x) + (3 * h)) / 2)) * (sin ((3 * h) / 2)))) ;
hence (fD (((sin (#) cos) (#) cos),h)) . x = (1 / 2) * (((cos (((2 * x) + h) / 2)) * (sin (h / 2))) + ((cos (((6 * x) + (3 * h)) / 2)) * (sin ((3 * h) / 2)))) ; :: thesis: verum