let Z be open Subset of REAL; :: thesis:
assume A1: Z c= dom (sin - ((1 / 3) (#) ((#Z 3) * sin))) ; :: thesis:
then Z c= (dom ((1 / 3) (#) ((#Z 3) * sin))) /\ (dom sin) by 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 by FDIFF_4:54;
A4: sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68;

now :: thesis:

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

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:19; :: thesis: