theorem Th45: :: HFDIFF_1:45

for x being Real st x <> 0 holds
( (id REAL) ^ is_differentiable_in x & diff (((id REAL) ^),x) = - (1 / (x ^2)) )