theorem Th4: :: FDIFF_5:4

for Z being open Subset of REAL st not 0 in Z holds
( (id Z) ^ is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) ^) `| Z) . x = - (1 / (x ^2)) ) )