theorem :: FDIFF_6:40

for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((- 2) (#) ((#R (1 / 2)) * (f + cos))) & ( for x being Real st x in Z holds
( f . x = 1 & sin . x > 0 & cos . x < 1 & cos . x > - 1 ) ) holds
( (- 2) (#) ((#R (1 / 2)) * (f + cos)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- 2) (#) ((#R (1 / 2)) * (f + cos))) `| Z) . x = (1 - (cos . x)) #R (1 / 2) ) )