let Z be open Subset of REAL; :: thesis: ( Z c= dom (() / exp_R) implies ( () / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((() / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)) / () ) ) )

A1: for x being Real st x in Z holds
exp_R . x <> 0 by SIN_COS:54;
assume Z c= dom (() / exp_R) ; :: thesis: ( () / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((() / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)) / () ) )

then Z c= (dom ()) /\ (() \ ()) by RFUNCT_1:def 1;
then A2: Z c= dom () by XBOOLE_1:18;
then A3: tan - cot is_differentiable_on Z by Th5;
A4: exp_R is_differentiable_on Z by ;
then A5: (tan - cot) / exp_R is_differentiable_on Z by ;
for x being Real st x in Z holds
((() / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)) / ()
proof
let x be Real; :: thesis: ( x in Z implies ((() / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)) / () )
A6: exp_R is_differentiable_in x by SIN_COS:65;
A7: exp_R . x <> 0 by SIN_COS:54;
assume A8: x in Z ; :: thesis: ((() / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)) / ()
then A9: (tan - cot) . x = (tan . x) - (cot . x) by ;
tan - cot is_differentiable_in x by ;
then diff ((() / exp_R),x) = (((diff ((),x)) * ()) - ((diff (exp_R,x)) * (() . x))) / (() ^2) by
.= ((((() `| Z) . x) * ()) - ((diff (exp_R,x)) * (() . x))) / (() ^2) by
.= ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) * ()) - ((diff (exp_R,x)) * (() . x))) / (() ^2) by A2, A8, Th5
.= ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) * ()) - (() * ((tan . x) - (cot . x)))) / (() * ()) by
.= (((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - ((tan . x) - (cot . x))) * (() / (() * ()))
.= (((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - ((tan . x) - (cot . x))) * ((() / ()) / ()) by XCMPLX_1:78
.= (((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - ((tan . x) - (cot . x))) * (1 / ()) by
.= (((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - ((tan . x) - (cot . x))) / () ;
hence (((tan - cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)) / () by ; :: thesis: verum
end;
hence ( (tan - cot) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((() / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)) / () ) ) by ; :: thesis: verum