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

then Z c= (dom ()) /\ () by VALUED_1:def 4;
then A2: Z c= dom () by XBOOLE_1:18;
then A3: tan + cot is_differentiable_on Z by Th6;
A4: exp_R is_differentiable_on Z by ;
for x being Real st x in Z holds
((exp_R (#) ()) `| Z) . x = (() * ((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 = (() * ((tan . x) + (cot . x))) + (() * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) )
assume A5: x in Z ; :: thesis: ((exp_R (#) ()) `| Z) . x = (() * ((tan . x) + (cot . x))) + (() * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))))
then ((exp_R (#) ()) `| Z) . x = ((() . x) * (diff (exp_R,x))) + (() * (diff ((),x))) by
.= (((tan . x) + (cot . x)) * (diff (exp_R,x))) + (() * (diff ((),x))) by
.= (() * ((tan . x) + (cot . x))) + (() * (diff ((),x))) by TAYLOR_1:16
.= (() * ((tan . x) + (cot . x))) + (() * ((() `| Z) . x)) by
.= (() * ((tan . x) + (cot . x))) + (() * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) by A2, A5, Th6 ;
hence ((exp_R (#) ()) `| Z) . x = (() * ((tan . x) + (cot . x))) + (() * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ; :: thesis: verum
end;
hence ( exp_R (#) () is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) ()) `| Z) . x = (() * ((tan . x) + (cot . x))) + (() * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) by ; :: thesis: verum