let Z be open Subset of REAL; :: thesis: ( Z c= dom ((- cos) - ((1 / 2) (#) ((#Z 2) * sin))) & ( for x being Real st x in Z holds
( sin . x > 0 & cos . x > - 1 ) ) implies ( (- cos) - ((1 / 2) (#) ((#Z 2) * sin)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cos) - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((sin . x) |^ 3) / (1 + (cos . x)) ) ) )
assume that
A1: Z c= dom ((- cos) - ((1 / 2) (#) ((#Z 2) * sin))) and
A2: for x being Real st x in Z holds
( sin . x > 0 & cos . x > - 1 ) ; :: thesis: ( (- cos) - ((1 / 2) (#) ((#Z 2) * sin)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cos) - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((sin . x) |^ 3) / (1 + (cos . x)) ) )
A3: Z c= (dom ((1 / 2) (#) ((#Z 2) * sin))) /\ (dom (- cos)) by A1, VALUED_1:12;
then A4: Z c= dom (- cos) by XBOOLE_1:18;
A5: Z c= dom ((1 / 2) (#) ((#Z 2) * sin)) by A3, XBOOLE_1:18;
then A6: (1 / 2) (#) ((#Z 2) * sin) is_differentiable_on Z by Th49;
A7: cos is_differentiable_on Z by FDIFF_1:26, SIN_COS:67;
A8: - cos is_differentiable_on Z by A4, A7, FDIFF_1:20;

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

let x be Real; :: thesis: ( x in Z implies (((- cos) - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((sin . x) |^ 3) / (1 + (cos . x)) )
assume A9: x in Z ; :: thesis: (((- cos) - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((sin . x) |^ 3) / (1 + (cos . x))
then A10: (cos . x) - (- 1) > 0 by A2, XREAL_1:50;
(((- cos) - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = (diff ((- cos),x)) - (diff (((1 / 2) (#) ((#Z 2) * sin)),x)) by A1, A6, A8, A9, FDIFF_1:19
.= (((- cos) `| Z) . x) - (diff (((1 / 2) (#) ((#Z 2) * sin)),x)) by A8, A9, FDIFF_1:def 7
.= ((- 1) * (diff (cos,x))) - (diff (((1 / 2) (#) ((#Z 2) * sin)),x)) by A4, A7, A9, FDIFF_1:20
.= ((- 1) * (- (sin . x))) - (diff (((1 / 2) (#) ((#Z 2) * sin)),x)) by SIN_COS:63
.= (sin . x) - ((((1 / 2) (#) ((#Z 2) * sin)) `| Z) . x) by A6, A9, FDIFF_1:def 7
.= (sin . x) - ((sin . x) * (cos . x)) by A5, A9, Th49
.= (((sin . x) * (1 - (cos . x))) * (1 + (cos . x))) / (1 + (cos . x)) by A10, XCMPLX_1:89
.= ((sin . x) * (1 - ((cos . x) ^2))) / (1 + (cos . x))
.= ((sin . x) * (1 - ((cos x) ^2))) / (1 + (cos . x)) by SIN_COS:def 19
.= ((sin . x) * ((sin x) * (sin x))) / (1 + (cos . x)) by SIN_COS4:4
.= ((sin . x) * ((sin x) |^ 2)) / (1 + (cos . x)) by WSIERP_1:1
.= ((sin . x) * ((sin . x) |^ 2)) / (1 + (cos . x)) by SIN_COS:def 17
.= ((sin . x) |^ (2 + 1)) / (1 + (cos . x)) by NEWTON:6
.= ((sin . x) |^ 3) / (1 + (cos . x)) ;
hence (((- cos) - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((sin . x) |^ 3) / (1 + (cos . x)) ; :: thesis: verum

end;

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