let Z be open Subset of REAL ; :: thesis: ( Z c= dom ((sin * ((id Z) ^ )) (#) (cos * ((id Z) ^ ))) & not 0 in Z implies ( (sin * ((id Z) ^ )) (#) (cos * ((id Z) ^ )) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * ((id Z) ^ )) (#) (cos * ((id Z) ^ ))) `| Z) . x = (1 / (x ^2 )) * (((sin . (1 / x)) ^2 ) - ((cos . (1 / x)) ^2 )) ) ) )
set f = id Z;
assume that
A1: Z c= dom ((sin * ((id Z) ^ )) (#) (cos * ((id Z) ^ ))) and
A2: not 0 in Z ; :: thesis: ( (sin * ((id Z) ^ )) (#) (cos * ((id Z) ^ )) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * ((id Z) ^ )) (#) (cos * ((id Z) ^ ))) `| Z) . x = (1 / (x ^2 )) * (((sin . (1 / x)) ^2 ) - ((cos . (1 / x)) ^2 )) ) )
A3: sin * ((id Z) ^ ) is_differentiable_on Z by A2, Th5;
A4: Z c= (dom (sin * ((id Z) ^ ))) /\ (dom (cos * ((id Z) ^ ))) by A1, VALUED_1:def 4;
then A5: Z c= dom (cos * ((id Z) ^ )) by XBOOLE_1:18;
then A6: cos * ((id Z) ^ ) is_differentiable_on Z by A2, Th6;
A7: 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 A8: Z c= dom ((id Z) ^ ) by TARSKI:def 3;

now

let x be Real; :: thesis: ( x in Z implies (((sin * ((id Z) ^ )) (#) (cos * ((id Z) ^ ))) `| Z) . x = (1 / (x ^2 )) * (((sin . (1 / x)) ^2 ) - ((cos . (1 / x)) ^2 )) )
assume A9: x in Z ; :: thesis: (((sin * ((id Z) ^ )) (#) (cos * ((id Z) ^ ))) `| Z) . x = (1 / (x ^2 )) * (((sin . (1 / x)) ^2 ) - ((cos . (1 / x)) ^2 ))
then (((sin * ((id Z) ^ )) (#) (cos * ((id Z) ^ ))) `| Z) . x = (((cos * ((id Z) ^ )) . x) * (diff (sin * ((id Z) ^ )),x)) + (((sin * ((id Z) ^ )) . x) * (diff (cos * ((id Z) ^ )),x)) by A1, A6, A3, FDIFF_1:29
.= (((cos * ((id Z) ^ )) . x) * (((sin * ((id Z) ^ )) `| Z) . x)) + (((sin * ((id Z) ^ )) . x) * (diff (cos * ((id Z) ^ )),x)) by A3, A9, FDIFF_1:def 8
.= (((cos * ((id Z) ^ )) . x) * (- ((1 / (x ^2 )) * (cos . (1 / x))))) + (((sin * ((id Z) ^ )) . x) * (diff (cos * ((id Z) ^ )),x)) by A2, A9, Th5
.= (((cos * ((id Z) ^ )) . x) * (- ((1 / (x ^2 )) * (cos . (1 / x))))) + (((sin * ((id Z) ^ )) . x) * (((cos * ((id Z) ^ )) `| Z) . x)) by A6, A9, FDIFF_1:def 8
.= (((cos * ((id Z) ^ )) . x) * (- ((1 / (x ^2 )) * (cos . (1 / x))))) + (((sin * ((id Z) ^ )) . x) * ((1 / (x ^2 )) * (sin . (1 / x)))) by A2, A5, A9, Th6
.= ((cos . (((id Z) ^ ) . x)) * (- ((1 / (x ^2 )) * (cos . (1 / x))))) + (((sin * ((id Z) ^ )) . x) * ((1 / (x ^2 )) * (sin . (1 / x)))) by A5, A9, FUNCT_1:22
.= ((cos . (((id Z) . x) " )) * (- ((1 / (x ^2 )) * (cos . (1 / x))))) + (((sin * ((id Z) ^ )) . x) * ((1 / (x ^2 )) * (sin . (1 / x)))) by A8, A9, RFUNCT_1:def 8
.= ((cos . (1 * (x " ))) * (- ((1 / (x ^2 )) * (cos . (1 / x))))) + (((sin * ((id Z) ^ )) . x) * ((1 / (x ^2 )) * (sin . (1 / x)))) by A9, FUNCT_1:35
.= ((cos . (1 / x)) * (- ((1 / (x ^2 )) * (cos . (1 / x))))) + (((sin * ((id Z) ^ )) . x) * ((1 / (x ^2 )) * (sin . (1 / x)))) by XCMPLX_0:def 9
.= ((cos . (1 / x)) * (- ((1 / (x ^2 )) * (cos . (1 / x))))) + ((sin . (((id Z) ^ ) . x)) * ((1 / (x ^2 )) * (sin . (1 / x)))) by A7, A9, FUNCT_1:22
.= ((cos . (1 / x)) * (- ((1 / (x ^2 )) * (cos . (1 / x))))) + ((sin . (((id Z) . x) " )) * ((1 / (x ^2 )) * (sin . (1 / x)))) by A8, A9, RFUNCT_1:def 8
.= ((cos . (1 / x)) * (- ((1 / (x ^2 )) * (cos . (1 / x))))) + ((sin . (1 * (x " ))) * ((1 / (x ^2 )) * (sin . (1 / x)))) by A9, FUNCT_1:35
.= (- (((cos . (1 / x)) * (1 / (x ^2 ))) * (cos . (1 / x)))) + ((sin . (1 / x)) * ((1 / (x ^2 )) * (sin . (1 / x)))) by XCMPLX_0:def 9
.= (1 / (x ^2 )) * (((sin . (1 / x)) ^2 ) - ((cos . (1 / x)) ^2 )) ;
hence (((sin * ((id Z) ^ )) (#) (cos * ((id Z) ^ ))) `| Z) . x = (1 / (x ^2 )) * (((sin . (1 / x)) ^2 ) - ((cos . (1 / x)) ^2 )) ; :: thesis: verum

end;

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