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 = (exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) ) ) )

assume A1: 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 = (exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) ) )

dom (exp_R * ()) c= dom () by RELAT_1:25;
then A2: Z c= dom () by ;
then A3: tan + cot is_differentiable_on Z by Th6;
A4: for x being Real st x in Z holds
exp_R * () is_differentiable_in x
proof end;
then A6: exp_R * () is_differentiable_on Z by ;
for x being Real st x in Z holds
((exp_R * ()) `| Z) . x = (exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))
proof
let x be Real; :: thesis: ( x in Z implies ((exp_R * ()) `| Z) . x = (exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) )
A7: exp_R is_differentiable_in () . x by SIN_COS:65;
assume A8: x in Z ; :: thesis: ((exp_R * ()) `| Z) . x = (exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))
then tan + cot is_differentiable_in x by ;
then diff ((exp_R * ()),x) = (diff (exp_R,(() . x))) * (diff ((),x)) by
.= (exp_R . (() . x)) * (diff ((),x)) by SIN_COS:65
.= (exp_R . (() . x)) * ((() `| Z) . x) by
.= (exp_R . (() . x)) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) by A2, A8, Th6
.= (exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) by ;
hence ((exp_R * ()) `| Z) . x = (exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) by ; :: thesis: verum
end;
hence ( exp_R * () is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * ()) `| Z) . x = (exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) ) ) by ; :: thesis: verum