let Z be open Subset of REAL; :: thesis: ( Z c= dom ((id Z) (#) (sin * ((id Z) ^))) & not 0 in Z implies ( (id Z) (#) (sin * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) (sin * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) - ((1 / x) * (cos . (1 / x))) ) ) )
set f = id Z;
assume that
A1: Z c= dom ((id Z) (#) (sin * ((id Z) ^))) and
A2: not 0 in Z ; :: thesis: ( (id Z) (#) (sin * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) (sin * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) - ((1 / x) * (cos . (1 / x))) ) )
A3: sin * ((id Z) ^) is_differentiable_on Z by A2, Th5;
A4: Z c= (dom (id Z)) /\ (dom (sin * ((id Z) ^))) by A1, VALUED_1:def 4;
then A5: Z c= dom (id Z) by XBOOLE_1:18;
A6: for x being Real st x in Z holds
(id Z) . x = (1 * x) + 0 by FUNCT_1:18;
then A7: id Z is_differentiable_on Z by A5, FDIFF_1:23;
A8: Z c= dom (sin * ((id Z) ^)) by A4, XBOOLE_1:18;
then for y being object st y in Z holds
y in dom ((id Z) ^) by FUNCT_1:11;
then A9: Z c= dom ((id Z) ^) ;

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

let x be Real; :: thesis: ( x in Z implies (((id Z) (#) (sin * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) - ((1 / x) * (cos . (1 / x))) )
assume A10: x in Z ; :: thesis: (((id Z) (#) (sin * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) - ((1 / x) * (cos . (1 / x)))
then (((id Z) (#) (sin * ((id Z) ^))) `| Z) . x = (((sin * ((id Z) ^)) . x) * (diff ((id Z),x))) + (((id Z) . x) * (diff ((sin * ((id Z) ^)),x))) by A1, A3, A7, FDIFF_1:21
.= (((sin * ((id Z) ^)) . x) * (((id Z) `| Z) . x)) + (((id Z) . x) * (diff ((sin * ((id Z) ^)),x))) by A7, A10, FDIFF_1:def 7
.= (((sin * ((id Z) ^)) . x) * 1) + (((id Z) . x) * (diff ((sin * ((id Z) ^)),x))) by A5, A6, A10, FDIFF_1:23
.= ((sin * ((id Z) ^)) . x) + (x * (diff ((sin * ((id Z) ^)),x))) by A10, FUNCT_1:18
.= ((sin * ((id Z) ^)) . x) + (x * (((sin * ((id Z) ^)) `| Z) . x)) by A3, A10, FDIFF_1:def 7
.= ((sin * ((id Z) ^)) . x) + (x * (- ((1 / (x ^2)) * (cos . (1 / x))))) by A2, A10, Th5
.= ((sin * ((id Z) ^)) . x) - ((x * (1 / (x * x))) * (cos . (1 / x)))
.= ((sin * ((id Z) ^)) . x) - ((x * ((1 / x) * (1 / x))) * (cos . (1 / x))) by XCMPLX_1:102
.= ((sin * ((id Z) ^)) . x) - (((x * (1 / x)) * (1 / x)) * (cos . (1 / x)))
.= ((sin * ((id Z) ^)) . x) - ((1 * (1 / x)) * (cos . (1 / x))) by A2, A10, XCMPLX_1:106
.= (sin . (((id Z) ^) . x)) - ((1 / x) * (cos . (1 / x))) by A8, A10, FUNCT_1:12
.= (sin . (((id Z) . x) ")) - ((1 / x) * (cos . (1 / x))) by A9, A10, RFUNCT_1:def 2
.= (sin . (1 * (x "))) - ((1 / x) * (cos . (1 / x))) by A10, FUNCT_1:18
.= (sin . (1 / x)) - ((1 / x) * (cos . (1 / x))) by XCMPLX_0:def 9 ;
hence (((id Z) (#) (sin * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) - ((1 / x) * (cos . (1 / x))) ; :: thesis: verum

end;

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