let Z be open Subset of REAL; :: thesis: ( Z c= dom (exp_R (#) (tan + cot)) implies ( exp_R (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) (tan + cot)) `| Z) . x = ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) )
assume A1: Z c= dom (exp_R (#) (tan + cot)) ; :: thesis: ( exp_R (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) (tan + cot)) `| Z) . x = ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) )
then Z c= (dom (tan + cot)) /\ (dom exp_R) by VALUED_1:def 4;
then A2: Z c= dom (tan + cot) by XBOOLE_1:18;
then A3: tan + cot is_differentiable_on Z by Th6;
A4: exp_R is_differentiable_on Z by FDIFF_1:26, TAYLOR_1:16;
for x being Real st x in Z holds
((exp_R (#) (tan + cot)) `| Z) . x = ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))))

proof

let x be Real; :: thesis: ( x in Z implies ((exp_R (#) (tan + cot)) `| Z) . x = ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) )
assume A5: x in Z ; :: thesis: ((exp_R (#) (tan + cot)) `| Z) . x = ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))))
then ((exp_R (#) (tan + cot)) `| Z) . x = (((tan + cot) . x) * (diff (exp_R,x))) + ((exp_R . x) * (diff ((tan + cot),x))) by A1, A3, A4, FDIFF_1:21
.= (((tan . x) + (cot . x)) * (diff (exp_R,x))) + ((exp_R . x) * (diff ((tan + cot),x))) by A2, A5, VALUED_1:def 1
.= ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * (diff ((tan + cot),x))) by TAYLOR_1:16
.= ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * (((tan + cot) `| Z) . x)) by A3, A5, FDIFF_1:def 7
.= ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) by A2, A5, Th6 ;
hence ((exp_R (#) (tan + cot)) `| Z) . x = ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ; :: thesis: verum

end;

hence ( exp_R (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) (tan + cot)) `| Z) . x = ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) by A1, A3, A4, FDIFF_1:21; :: thesis: verum