theorem Th47: :: HFDIFF_1:47

for x being Real st x <> 0 holds
( (#Z 2) ^ is_differentiable_in x & diff (((#Z 2) ^),x) = - ((2 * x) / ((x #Z 2) ^2)) )