let f1, f2 be PartFunc of REAL ,REAL ; :: thesis: 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 )) ) )
let Z be open Subset of REAL ; :: thesis: ( Z c= dom ((f1 + f2) ^ ) & ( for x being Real st x in Z holds
f1 . x = 1 ) & f2 = #Z 2 implies ( (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 )) ) ) )
assume A1: ( Z c= dom ((f1 + f2) ^ ) & ( for x being Real st x in Z holds
f1 . x = 1 ) & f2 = #Z 2 ) ; :: thesis: ( (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 )) ) )
A2: dom ((f1 + f2) ^ ) c= dom (f1 + f2) by RFUNCT_1:11;
A3: Z c= dom (f1 + f2) by A1, A2, XBOOLE_1:1;
A4: ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 + f2) `| Z) . x = 2 * x ) ) by A1, A3, SIN_COS9:101;
A5: for x being Real st x in Z holds
(f1 + f2) . x <> 0 by RFUNCT_1:13, A1;
A6: (f1 + f2) ^ is_differentiable_on Z by A4, A5, FDIFF_2:22;
for x being Real st x in Z holds
(((f1 + f2) ^ ) `| Z) . x = - ((2 * x) / ((1 + (x |^ 2)) ^2 ))

proof

let x be Real; :: thesis: ( x in Z implies (((f1 + f2) ^ ) `| Z) . x = - ((2 * x) / ((1 + (x |^ 2)) ^2 )) )
assume A7: x in Z ; :: thesis: (((f1 + f2) ^ ) `| Z) . x = - ((2 * x) / ((1 + (x |^ 2)) ^2 ))
then A8: (f1 + f2) . x <> 0 by RFUNCT_1:13, A1;
A9: f1 + f2 is_differentiable_in x by A4, A7, FDIFF_1:16;
A10: f2 . x = x #Z 2 by A1, TAYLOR_1:def 1
.= x |^ 2 by PREPOWER:46 ;
A11: (f1 + f2) . x = (f1 . x) + (f2 . x) by A3, A7, VALUED_1:def 1
.= 1 + (x |^ 2) by A1, A7, A10 ;
(((f1 + f2) ^ ) `| Z) . x = diff ((f1 + f2) ^ ),x by A6, A7, FDIFF_1:def 8
.= - ((diff (f1 + f2),x) / (((f1 + f2) . x) ^2 )) by A8, A9, FDIFF_2:15
.= - ((((f1 + f2) `| Z) . x) / (((f1 + f2) . x) ^2 )) by A4, A7, FDIFF_1:def 8
.= - ((2 * x) / ((1 + (x |^ 2)) ^2 )) by A1, A3, SIN_COS9:101, A7, A11 ;
hence (((f1 + f2) ^ ) `| Z) . x = - ((2 * x) / ((1 + (x |^ 2)) ^2 )) ; :: thesis: verum

end;

hence ( (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 )) ) ) by A4, A5, FDIFF_2:22; :: thesis: verum