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 A1: ( Z c= dom ((sin * ((id Z) ^ )) (#) (cos * ((id Z) ^ ))) & 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 )) ) )
AA: for x being Real st x in Z holds
(id Z) . x = x by FUNCT_1:35;
Z c= (dom (sin * ((id Z) ^ ))) /\ (dom (cos * ((id Z) ^ ))) by A1, VALUED_1:def 4;
then A2: ( Z c= dom (sin * ((id Z) ^ )) & Z c= dom (cos * ((id Z) ^ )) ) by XBOOLE_1:18;
then for y being set st y in Z holds
y in dom ((id Z) ^ ) by FUNCT_1:21;
then A3: Z c= dom ((id Z) ^ ) by TARSKI:def 3;
A4: ( cos * ((id Z) ^ ) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * ((id Z) ^ )) `| Z) . x = (1 / (x ^2 )) * (sin . (1 / x)) ) ) by A1, A2, Th6;
A5: ( sin * ((id Z) ^ ) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * ((id Z) ^ )) `| Z) . x = - ((1 / (x ^2 )) * (cos . (1 / x))) ) ) by A1, Th5;

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 A6: 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, A4, A5, FDIFF_1:29
.= (((cos * ((id Z) ^ )) . x) * (((sin * ((id Z) ^ )) `| Z) . x)) + (((sin * ((id Z) ^ )) . x) * (diff (cos * ((id Z) ^ )),x)) by A5, A6, FDIFF_1:def 8
.= (((cos * ((id Z) ^ )) . x) * (- ((1 / (x ^2 )) * (cos . (1 / x))))) + (((sin * ((id Z) ^ )) . x) * (diff (cos * ((id Z) ^ )),x)) by A1, A6, Th5
.= (((cos * ((id Z) ^ )) . x) * (- ((1 / (x ^2 )) * (cos . (1 / x))))) + (((sin * ((id Z) ^ )) . x) * (((cos * ((id Z) ^ )) `| Z) . x)) by A4, A6, 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 A1, A2, A6, Th6
.= ((cos . (((id Z) ^ ) . x)) * (- ((1 / (x ^2 )) * (cos . (1 / x))))) + (((sin * ((id Z) ^ )) . x) * ((1 / (x ^2 )) * (sin . (1 / x)))) by A2, A6, FUNCT_1:22
.= ((cos . (((id Z) . x) " )) * (- ((1 / (x ^2 )) * (cos . (1 / x))))) + (((sin * ((id Z) ^ )) . x) * ((1 / (x ^2 )) * (sin . (1 / x)))) by A3, A6, RFUNCT_1:def 8
.= ((cos . (1 * (x " ))) * (- ((1 / (x ^2 )) * (cos . (1 / x))))) + (((sin * ((id Z) ^ )) . x) * ((1 / (x ^2 )) * (sin . (1 / x)))) by A6, AA
.= ((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 A2, A6, FUNCT_1:22
.= ((cos . (1 / x)) * (- ((1 / (x ^2 )) * (cos . (1 / x))))) + ((sin . (((id Z) . x) " )) * ((1 / (x ^2 )) * (sin . (1 / x)))) by A3, A6, RFUNCT_1:def 8
.= ((cos . (1 / x)) * (- ((1 / (x ^2 )) * (cos . (1 / x))))) + ((sin . (1 * (x " ))) * ((1 / (x ^2 )) * (sin . (1 / x)))) by A6, AA
.= (- (((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, A4, A5, FDIFF_1:29; :: thesis: verum