let Z be open Subset of REAL; ( Z c= dom (((- (id Z)) (#) cos) + sin) implies ( ((- (id Z)) (#) cos) + sin is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (id Z)) (#) cos) + sin) `| Z) . x = x * (sin . x) ) ) )
assume A1:
Z c= dom (((- (id Z)) (#) cos) + sin)
; ( ((- (id Z)) (#) cos) + sin is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (id Z)) (#) cos) + sin) `| Z) . x = x * (sin . x) ) )
then
Z c= (dom ((- (id Z)) (#) cos)) /\ (dom sin)
by VALUED_1:def 1;
then A2:
Z c= dom ((- (id Z)) (#) cos)
by XBOOLE_1:18;
then A3:
(- (id Z)) (#) cos is_differentiable_on Z
by Th44;
A4:
sin is_differentiable_on Z
by FDIFF_1:26, SIN_COS:68;
now for x being Real st x in Z holds
((((- (id Z)) (#) cos) + sin) `| Z) . x = x * (sin . x)let x be
Real;
( x in Z implies ((((- (id Z)) (#) cos) + sin) `| Z) . x = x * (sin . x) )assume A5:
x in Z
;
((((- (id Z)) (#) cos) + sin) `| Z) . x = x * (sin . x)hence ((((- (id Z)) (#) cos) + sin) `| Z) . x =
(diff (((- (id Z)) (#) cos),x)) + (diff (sin,x))
by A1, A3, A4, FDIFF_1:18
.=
((((- (id Z)) (#) cos) `| Z) . x) + (diff (sin,x))
by A3, A5, FDIFF_1:def 7
.=
((- (cos . x)) + (x * (sin . x))) + (diff (sin,x))
by A2, A5, Th44
.=
((- (cos . x)) + (x * (sin . x))) + (cos . x)
by SIN_COS:64
.=
x * (sin . x)
;
verum end;
hence
( ((- (id Z)) (#) cos) + sin is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (id Z)) (#) cos) + sin) `| Z) . x = x * (sin . x) ) )
by A1, A3, A4, FDIFF_1:18; verum