let Z be open Subset of REAL; :: thesis: ( Z c= dom (((1 / 3) (#) ((#Z 3) * cos)) - cos) 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 A1: Z c= dom (((1 / 3) (#) ((#Z 3) * cos)) - cos) ; :: 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 ) )
then Z c= (dom ((1 / 3) (#) ((#Z 3) * cos))) /\ (dom cos) by VALUED_1:12;
then A2: Z c= dom ((1 / 3) (#) ((#Z 3) * cos)) by XBOOLE_1:18;
then A3: (1 / 3) (#) ((#Z 3) * cos) is_differentiable_on Z by Th46;
A4: cos is_differentiable_on Z by FDIFF_1:26, SIN_COS:67;

now :: thesis: for x being Real st x in Z holds
((((1 / 3) (#) ((#Z 3) * cos)) - cos) `| Z) . x = (sin . x) |^ 3

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:19
.= (diff (((1 / 3) (#) ((#Z 3) * cos)),x)) - (- (sin . x)) by SIN_COS:63
.= ((((1 / 3) (#) ((#Z 3) * cos)) `| Z) . x) - (- (sin . x)) by A3, A5, FDIFF_1:def 7
.= (- (((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) |^ |.2.|)) by PREPOWER:def 3
.= (sin . x) * (1 - ((cos . x) |^ 2)) by ABSVALUE:def 1
.= (sin . x) * (1 - ((cos . x) * (cos . x))) by WSIERP_1:1
.= (sin . x) * ((((cos . x) * (cos . x)) + ((sin . x) * (sin . x))) - ((cos . x) * (cos . x))) by SIN_COS:28
.= (sin . x) * ((sin . x) |^ 2) by WSIERP_1:1
.= (sin . x) |^ (2 + 1) by NEWTON:6
.= (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:19; :: thesis: verum