let Z be open Subset of REAL; ( Z c= dom (sin - ((1 / 2) (#) ((#Z 2) * sin))) & ( for x being Real st x in Z holds
( sin . x > 0 & sin . x > - 1 ) ) implies ( sin - ((1 / 2) (#) ((#Z 2) * sin)) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 + (sin . x)) ) ) )
assume that
A1:
Z c= dom (sin - ((1 / 2) (#) ((#Z 2) * sin)))
and
A2:
for x being Real st x in Z holds
( sin . x > 0 & sin . x > - 1 )
; ( sin - ((1 / 2) (#) ((#Z 2) * sin)) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 + (sin . x)) ) )
Z c= (dom ((1 / 2) (#) ((#Z 2) * sin))) /\ (dom sin)
by A1, VALUED_1:12;
then A3:
Z c= dom ((1 / 2) (#) ((#Z 2) * sin))
by XBOOLE_1:18;
then A4:
(1 / 2) (#) ((#Z 2) * sin) is_differentiable_on Z
by Th49;
A5:
sin is_differentiable_on Z
by FDIFF_1:26, SIN_COS:68;
now for x being Real st x in Z holds
((sin - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 + (sin . x))let x be
Real;
( x in Z implies ((sin - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 + (sin . x)) )assume A6:
x in Z
;
((sin - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 + (sin . x))then
sin . x > - 1
by A2;
then A7:
(sin . x) - (- 1) > 0
by XREAL_1:50;
((sin - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x =
(diff (sin,x)) - (diff (((1 / 2) (#) ((#Z 2) * sin)),x))
by A1, A4, A5, A6, FDIFF_1:19
.=
(cos . x) - (diff (((1 / 2) (#) ((#Z 2) * sin)),x))
by SIN_COS:64
.=
(cos . x) - ((((1 / 2) (#) ((#Z 2) * sin)) `| Z) . x)
by A4, A6, FDIFF_1:def 7
.=
(cos . x) - ((sin . x) * (cos . x))
by A3, A6, Th49
.=
(((cos . x) * (1 - (sin . x))) * (1 + (sin . x))) / (1 + (sin . x))
by A7, XCMPLX_1:89
.=
((cos . x) * (1 - ((sin . x) ^2))) / (1 + (sin . x))
.=
((cos . x) * (1 - ((sin x) ^2))) / (1 + (sin . x))
by SIN_COS:def 17
.=
((cos . x) * ((cos x) * (cos x))) / (1 + (sin . x))
by SIN_COS4:5
.=
((cos . x) * ((cos x) |^ 2)) / (1 + (sin . x))
by WSIERP_1:1
.=
((cos . x) * ((cos . x) |^ 2)) / (1 + (sin . x))
by SIN_COS:def 19
.=
((cos . x) |^ (2 + 1)) / (1 + (sin . x))
by NEWTON:6
.=
((cos . x) |^ 3) / (1 + (sin . x))
;
hence
((sin - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 + (sin . x))
;
verum end;
hence
( sin - ((1 / 2) (#) ((#Z 2) * sin)) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 + (sin . x)) ) )
by A1, A4, A5, FDIFF_1:19; verum