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

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

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

end;

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