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

now

let x be Real; :: thesis: ( x in Z implies (((sin * (f ^ )) (#) (cos * (f ^ ))) `| Z) . x = (1 / (x ^2 )) * (((sin . (1 / x)) ^2 ) - ((cos . (1 / x)) ^2 )) )
assume A6: x in Z ; :: thesis: (((sin * (f ^ )) (#) (cos * (f ^ ))) `| Z) . x = (1 / (x ^2 )) * (((sin . (1 / x)) ^2 ) - ((cos . (1 / x)) ^2 ))
then (((sin * (f ^ )) (#) (cos * (f ^ ))) `| Z) . x = (((cos * (f ^ )) . x) * (diff (sin * (f ^ )),x)) + (((sin * (f ^ )) . x) * (diff (cos * (f ^ )),x)) by A1, A4, A5, FDIFF_1:29
.= (((cos * (f ^ )) . x) * (((sin * (f ^ )) `| Z) . x)) + (((sin * (f ^ )) . x) * (diff (cos * (f ^ )),x)) by A5, A6, FDIFF_1:def 8
.= (((cos * (f ^ )) . x) * (- ((1 / (x ^2 )) * (cos . (1 / x))))) + (((sin * (f ^ )) . x) * (diff (cos * (f ^ )),x)) by A1, A2, A6, Th5
.= (((cos * (f ^ )) . x) * (- ((1 / (x ^2 )) * (cos . (1 / x))))) + (((sin * (f ^ )) . x) * (((cos * (f ^ )) `| Z) . x)) by A4, A6, FDIFF_1:def 8
.= (((cos * (f ^ )) . x) * (- ((1 / (x ^2 )) * (cos . (1 / x))))) + (((sin * (f ^ )) . x) * ((1 / (x ^2 )) * (sin . (1 / x)))) by A1, A2, A6, Th6
.= ((cos . ((f ^ ) . x)) * (- ((1 / (x ^2 )) * (cos . (1 / x))))) + (((sin * (f ^ )) . x) * ((1 / (x ^2 )) * (sin . (1 / x)))) by A2, A6, FUNCT_1:22
.= ((cos . ((f . x) " )) * (- ((1 / (x ^2 )) * (cos . (1 / x))))) + (((sin * (f ^ )) . x) * ((1 / (x ^2 )) * (sin . (1 / x)))) by A3, A6, RFUNCT_1:def 8
.= ((cos . (1 * (x " ))) * (- ((1 / (x ^2 )) * (cos . (1 / x))))) + (((sin * (f ^ )) . x) * ((1 / (x ^2 )) * (sin . (1 / x)))) by A1, A6
.= ((cos . (1 / x)) * (- ((1 / (x ^2 )) * (cos . (1 / x))))) + (((sin * (f ^ )) . x) * ((1 / (x ^2 )) * (sin . (1 / x)))) by XCMPLX_0:def 9
.= ((cos . (1 / x)) * (- ((1 / (x ^2 )) * (cos . (1 / x))))) + ((sin . ((f ^ ) . x)) * ((1 / (x ^2 )) * (sin . (1 / x)))) by A2, A6, FUNCT_1:22
.= ((cos . (1 / x)) * (- ((1 / (x ^2 )) * (cos . (1 / x))))) + ((sin . ((f . 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 A1, A6
.= (- (((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 * (f ^ )) (#) (cos * (f ^ ))) `| Z) . x = (1 / (x ^2 )) * (((sin . (1 / x)) ^2 ) - ((cos . (1 / x)) ^2 )) ; :: thesis: verum

end;

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