let n be Element of NAT ; :: thesis: for Z being open Subset of REAL st Z c= dom (((1 / 3) (#) ((#Z 3) * cos )) - cos ) & n > 0 holds
( ((1 / 3) (#) ((#Z 3) * cos )) - cos is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / 3) (#) ((#Z 3) * cos )) - cos ) `| Z) . x = (sin . x) |^ 3 ) )
let Z be open Subset of REAL ; :: thesis: ( Z c= dom (((1 / 3) (#) ((#Z 3) * cos )) - cos ) & n > 0 implies ( ((1 / 3) (#) ((#Z 3) * cos )) - cos is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / 3) (#) ((#Z 3) * cos )) - cos ) `| Z) . x = (sin . x) |^ 3 ) ) )
assume that
A1: Z c= dom (((1 / 3) (#) ((#Z 3) * cos )) - cos ) and
n > 0 ; :: thesis: ( ((1 / 3) (#) ((#Z 3) * cos )) - cos is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / 3) (#) ((#Z 3) * cos )) - cos ) `| Z) . x = (sin . x) |^ 3 ) )
Z c= (dom ((1 / 3) (#) ((#Z 3) * cos ))) /\ (dom cos ) by A1, VALUED_1:12;
then A2: ( Z c= dom ((1 / 3) (#) ((#Z 3) * cos )) & Z c= dom cos ) by XBOOLE_1:18;
then A3: ( (1 / 3) (#) ((#Z 3) * cos ) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 3) (#) ((#Z 3) * cos )) `| Z) . x = - (((cos . x) #Z (3 - 1)) * (sin . x)) ) ) by Th46;
A4: cos is_differentiable_on Z by FDIFF_1:34, SIN_COS:72;

now

let x be Real; :: thesis: ( x in Z implies ((((1 / 3) (#) ((#Z 3) * cos )) - cos ) `| Z) . x = (sin . x) |^ 3 )
assume A5: x in Z ; :: thesis: ((((1 / 3) (#) ((#Z 3) * cos )) - cos ) `| Z) . x = (sin . x) |^ 3
then ((((1 / 3) (#) ((#Z 3) * cos )) - cos ) `| Z) . x = (diff ((1 / 3) (#) ((#Z 3) * cos )),x) - (diff cos ,x) by A1, A3, A4, FDIFF_1:27
.= (diff ((1 / 3) (#) ((#Z 3) * cos )),x) - (- (sin . x)) by SIN_COS:68
.= ((((1 / 3) (#) ((#Z 3) * cos )) `| Z) . x) - (- (sin . x)) by A3, A5, FDIFF_1:def 8
.= (- (((cos . x) #Z (3 - 1)) * (sin . x))) - (- (sin . x)) by A2, A5, Th46
.= (sin . x) * (1 - ((cos . x) #Z 2))
.= (sin . x) * (1 - ((cos . x) |^ (abs 2))) by PREPOWER:def 4
.= (sin . x) * (1 - ((cos . x) |^ 2)) by ABSVALUE:def 1
.= (sin . x) * (1 - ((cos . x) * (cos . x))) by WSIERP_1:2
.= (sin . x) * ((((cos . x) * (cos . x)) + ((sin . x) * (sin . x))) - ((cos . x) * (cos . x))) by SIN_COS:31
.= (sin . x) * ((sin . x) |^ 2) by WSIERP_1:2
.= (sin . x) |^ (2 + 1) by NEWTON:11
.= (sin . x) |^ 3 ;
hence ((((1 / 3) (#) ((#Z 3) * cos )) - cos ) `| Z) . x = (sin . x) |^ 3 ; :: thesis: verum

end;

hence ( ((1 / 3) (#) ((#Z 3) * cos )) - cos is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / 3) (#) ((#Z 3) * cos )) - cos ) `| Z) . x = (sin . x) |^ 3 ) ) by A1, A3, A4, FDIFF_1:27; :: thesis: verum