theorem Th2: :: LEIBNIZ1:2

for r being Real holds diff (arctan,r) = 1 / (1 + (r ^2))