let a be Real; :: thesis: for Z being open Subset of REAL

for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 + f2) & ( for x being Real st x in Z holds

f1 . x = a ) & 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 ) )

let Z be open Subset of REAL; :: thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 + f2) & ( for x being Real st x in Z holds

f1 . x = a ) & 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 ) )

let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( Z c= dom (f1 + f2) & ( for x being Real st x in Z holds

f1 . x = a ) & 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 ) ) )

assume that

A1: Z c= dom (f1 + f2) and

A2: for x being Real st x in Z holds

f1 . x = a and

A3: 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 ) )

A4: for x being Real st x in Z holds

f2 is_differentiable_in x by A3, TAYLOR_1:2;

A5: Z c= (dom f1) /\ (dom f2) by A1, VALUED_1:def 1;

then A6: Z c= dom f1 by XBOOLE_1:18;

A7: for x being Real st x in Z holds

f1 . x = (0 * x) + a by A2;

then A8: f1 is_differentiable_on Z by A6, FDIFF_1:23;

Z c= dom f2 by A5, XBOOLE_1:18;

then A9: f2 is_differentiable_on Z by A4, FDIFF_1:9;

A10: for x being Real st x in Z holds

(f2 `| Z) . x = 2 * (x #Z (2 - 1))

((f1 + f2) `| Z) . x = 2 * x

((f1 + f2) `| Z) . x = 2 * x ) ) by A1, A8, A9, FDIFF_1:18; :: thesis: verum

for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 + f2) & ( for x being Real st x in Z holds

f1 . x = a ) & 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 ) )

let Z be open Subset of REAL; :: thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 + f2) & ( for x being Real st x in Z holds

f1 . x = a ) & 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 ) )

let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( Z c= dom (f1 + f2) & ( for x being Real st x in Z holds

f1 . x = a ) & 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 ) ) )

assume that

A1: Z c= dom (f1 + f2) and

A2: for x being Real st x in Z holds

f1 . x = a and

A3: 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 ) )

A4: for x being Real st x in Z holds

f2 is_differentiable_in x by A3, TAYLOR_1:2;

A5: Z c= (dom f1) /\ (dom f2) by A1, VALUED_1:def 1;

then A6: Z c= dom f1 by XBOOLE_1:18;

A7: for x being Real st x in Z holds

f1 . x = (0 * x) + a by A2;

then A8: f1 is_differentiable_on Z by A6, FDIFF_1:23;

Z c= dom f2 by A5, XBOOLE_1:18;

then A9: f2 is_differentiable_on Z by A4, FDIFF_1:9;

A10: for x being Real st x in Z holds

(f2 `| Z) . x = 2 * (x #Z (2 - 1))

proof

for x being Real st x in Z holds
let x be Real; :: thesis: ( x in Z implies (f2 `| Z) . x = 2 * (x #Z (2 - 1)) )

assume A11: x in Z ; :: thesis: (f2 `| Z) . x = 2 * (x #Z (2 - 1))

diff (f2,x) = 2 * (x #Z (2 - 1)) by A3, TAYLOR_1:2;

hence (f2 `| Z) . x = 2 * (x #Z (2 - 1)) by A9, A11, FDIFF_1:def 7; :: thesis: verum

end;assume A11: x in Z ; :: thesis: (f2 `| Z) . x = 2 * (x #Z (2 - 1))

diff (f2,x) = 2 * (x #Z (2 - 1)) by A3, TAYLOR_1:2;

hence (f2 `| Z) . x = 2 * (x #Z (2 - 1)) by A9, A11, FDIFF_1:def 7; :: thesis: verum

((f1 + f2) `| Z) . x = 2 * x

proof

hence
( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds
let x be Real; :: thesis: ( x in Z implies ((f1 + f2) `| Z) . x = 2 * x )

assume A12: x in Z ; :: thesis: ((f1 + f2) `| Z) . x = 2 * x

then ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) by A1, A8, A9, FDIFF_1:18;

hence ((f1 + f2) `| Z) . x = ((f1 `| Z) . x) + (diff (f2,x)) by A8, A12, FDIFF_1:def 7

.= ((f1 `| Z) . x) + ((f2 `| Z) . x) by A9, A12, FDIFF_1:def 7

.= 0 + ((f2 `| Z) . x) by A6, A7, A12, FDIFF_1:23

.= 2 * (x #Z (2 - 1)) by A10, A12

.= 2 * (x |^ 1) by PREPOWER:36

.= 2 * x ;

:: thesis: verum

end;assume A12: x in Z ; :: thesis: ((f1 + f2) `| Z) . x = 2 * x

then ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) by A1, A8, A9, FDIFF_1:18;

hence ((f1 + f2) `| Z) . x = ((f1 `| Z) . x) + (diff (f2,x)) by A8, A12, FDIFF_1:def 7

.= ((f1 `| Z) . x) + ((f2 `| Z) . x) by A9, A12, FDIFF_1:def 7

.= 0 + ((f2 `| Z) . x) by A6, A7, A12, FDIFF_1:23

.= 2 * (x #Z (2 - 1)) by A10, A12

.= 2 * (x |^ 1) by PREPOWER:36

.= 2 * x ;

:: thesis: verum

((f1 + f2) `| Z) . x = 2 * x ) ) by A1, A8, A9, FDIFF_1:18; :: thesis: verum