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

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

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