theorem Th1: :: INTEGR12:1

for f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st Z c= dom ((f1 + f2) ^) & ( for x being Real st x in Z holds
f1 . x = 1 ) & f2 = #Z 2 holds
( (f1 + f2) ^ is_differentiable_on Z & ( for x being Real st x in Z holds
(((f1 + f2) ^) `| Z) . x = - ((2 * x) / ((1 + (x |^ 2)) ^2)) ) )