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

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

dom (cos * ()) 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
cos * () is_differentiable_in x
proof end;
then A6: cos * () is_differentiable_on Z by ;
for x being Real st x in Z holds
((cos * ()) `| Z) . x = - ((sin . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))))
proof
let x be Real; :: thesis: ( x in Z implies ((cos * ()) `| Z) . x = - ((sin . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) )
A7: cos is_differentiable_in () . x by SIN_COS:63;
assume A8: x in Z ; :: thesis: ((cos * ()) `| Z) . x = - ((sin . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))))
then tan + cot is_differentiable_in x by ;
then diff ((cos * ()),x) = (diff (cos,(() . x))) * (diff ((),x)) by
.= (- (sin . (() . x))) * (diff ((),x)) by SIN_COS:63
.= (- (sin . (() . x))) * ((() `| Z) . x) by
.= (- (sin . (() . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) by A2, A8, Th6
.= (- (sin . ((tan . x) + (cot . x)))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) by ;
hence ((cos * ()) `| Z) . x = - ((sin . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) by ; :: thesis: verum
end;
hence ( cos * () is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * ()) `| Z) . x = - ((sin . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) by ; :: thesis: verum