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:35;
then A7: id Z is_differentiable_on Z by A5, FDIFF_1:31;
A8: Z c= dom (sin * ((id Z) ^ )) by A4, XBOOLE_1:18;
then for y being set st y in Z holds
y in dom ((id Z) ^ ) by FUNCT_1:21;
then A9: Z c= dom ((id Z) ^ ) by TARSKI:def 3;

now

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:29
.= (((sin * ((id Z) ^ )) . x) * (((id Z) `| Z) . x)) + (((id Z) . x) * (diff (sin * ((id Z) ^ )),x)) by A7, A10, FDIFF_1:def 8
.= (((sin * ((id Z) ^ )) . x) * 1) + (((id Z) . x) * (diff (sin * ((id Z) ^ )),x)) by A5, A6, A10, FDIFF_1:31
.= ((sin * ((id Z) ^ )) . x) + (x * (diff (sin * ((id Z) ^ )),x)) by A10, FUNCT_1:35
.= ((sin * ((id Z) ^ )) . x) + (x * (((sin * ((id Z) ^ )) `| Z) . x)) by A3, A10, FDIFF_1:def 8
.= ((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:103
.= ((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:107
.= (sin . (((id Z) ^ ) . x)) - ((1 / x) * (cos . (1 / x))) by A8, A10, FUNCT_1:22
.= (sin . (((id Z) . x) " )) - ((1 / x) * (cos . (1 / x))) by A9, A10, RFUNCT_1:def 8
.= (sin . (1 * (x " ))) - ((1 / x) * (cos . (1 / x))) by A10, FUNCT_1:35
.= (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:29; :: thesis: verum