theorem Th7: :: FDIFF_7:7

for x being Real
for f being PartFunc of REAL,REAL st f is_differentiable_in x & f . x > - 1 & f . x < 1 holds
( arccos * f is_differentiable_in x & diff ((arccos * f),x) = - ((diff (f,x)) / (sqrt (1 - ((f . x) ^2)))) )