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

now

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

end;

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