theorem Th13: :: LEIBNIZ1:13

for r being Real st 0 <= r & r <= 1 holds
arctan . r = Sum (Leibniz_Series_of r)