let X be set ; :: thesis: for f, g, F, G being PartFunc of REAL,REAL st F is_integral_of f,X & G is_integral_of g,X holds
( F + G is_integral_of f + g,X & F - G is_integral_of f - g,X )
let f, g, F, G be PartFunc of REAL,REAL; :: thesis: ( F is_integral_of f,X & G is_integral_of g,X implies ( F + G is_integral_of f + g,X & F - G is_integral_of f - g,X ) )
assume that
A1: F is_integral_of f,X and
A2: G is_integral_of g,X ; :: thesis: ( F + G is_integral_of f + g,X & F - G is_integral_of f - g,X )
A3: G is_differentiable_on X by A2, Lm1;
A4: G `| X = g | X by A2, Lm1;
then dom (g | X) = X by A3, FDIFF_1:def 7;
then (dom g) /\ X = X by RELAT_1:61;
then A5: X c= dom g by XBOOLE_1:18;
A6: F is_differentiable_on X by A1, Lm1;
then A7: F + G is_differentiable_on X by A3, Th6;
A8: F `| X = f | X by A1, Lm1;
then dom (f | X) = X by A6, FDIFF_1:def 7;
then (dom f) /\ X = X by RELAT_1:61;
then X c= dom f by XBOOLE_1:18;
then A9: X c= (dom f) /\ (dom g) by A5, XBOOLE_1:19;
then A10: X c= dom (f + g) by VALUED_1:def 1;

A11: now :: thesis: for x being Element of REAL st x in dom ((F + G) `| X) holds
((F + G) `| X) . x = ((f + g) | X) . x

let x be Element of REAL ; :: thesis: ( x in dom ((F + G) `| X) implies ((F + G) `| X) . x = ((f + g) | X) . x )
assume x in dom ((F + G) `| X) ; :: thesis: ((F + G) `| X) . x = ((f + g) | X) . x
then A12: x in X by A7, FDIFF_1:def 7;
then F | X is_differentiable_in x by A6;
then A13: F is_differentiable_in x by A12, Th4;
(G `| X) . x = diff (G,x) by A3, A12, FDIFF_1:def 7;
then A14: g . x = diff (G,x) by A4, A12, FUNCT_1:49;
(F `| X) . x = diff (F,x) by A6, A12, FDIFF_1:def 7;
then A15: f . x = diff (F,x) by A8, A12, FUNCT_1:49;
G | X is_differentiable_in x by A3, A12;
then A16: G is_differentiable_in x by A12, Th4;
((F + G) `| X) . x = diff ((F + G),x) by A7, A12, FDIFF_1:def 7;
then ((F + G) `| X) . x = (diff (F,x)) + (diff (G,x)) by A13, A16, FDIFF_1:13;
then ((F + G) `| X) . x = (f + g) . x by A10, A12, A15, A14, VALUED_1:def 1;
hence ((F + G) `| X) . x = ((f + g) | X) . x by A12, FUNCT_1:49; :: thesis: verum

end;

A17: F - G is_differentiable_on X by A6, A3, Th6;
A18: X c= dom (f - g) by A9, VALUED_1:12;

A19: now :: thesis: for x being Element of REAL st x in dom ((F - G) `| X) holds
((F - G) `| X) . x = ((f - g) | X) . x

let x be Element of REAL ; :: thesis: ( x in dom ((F - G) `| X) implies ((F - G) `| X) . x = ((f - g) | X) . x )
assume x in dom ((F - G) `| X) ; :: thesis: ((F - G) `| X) . x = ((f - g) | X) . x
then A20: x in X by A17, FDIFF_1:def 7;
then F | X is_differentiable_in x by A6;
then A21: F is_differentiable_in x by A20, Th4;
(G `| X) . x = diff (G,x) by A3, A20, FDIFF_1:def 7;
then A22: g . x = diff (G,x) by A4, A20, FUNCT_1:49;
(F `| X) . x = diff (F,x) by A6, A20, FDIFF_1:def 7;
then A23: f . x = diff (F,x) by A8, A20, FUNCT_1:49;
G | X is_differentiable_in x by A3, A20;
then A24: G is_differentiable_in x by A20, Th4;
((F - G) `| X) . x = diff ((F - G),x) by A17, A20, FDIFF_1:def 7;
then ((F - G) `| X) . x = (diff (F,x)) - (diff (G,x)) by A21, A24, FDIFF_1:14;
then ((F - G) `| X) . x = (f - g) . x by A18, A20, A23, A22, VALUED_1:13;
hence ((F - G) `| X) . x = ((f - g) | X) . x by A20, FUNCT_1:49; :: thesis: verum

end;

X = dom ((f + g) | X) by A10, RELAT_1:62;
then dom ((F + G) `| X) = dom ((f + g) | X) by A7, FDIFF_1:def 7;
then (F + G) `| X = (f + g) | X by A11, PARTFUN1:5;
hence F + G is_integral_of f + g,X by A7, Lm1; :: thesis: F - G is_integral_of f - g,X
X = dom ((f - g) | X) by A18, RELAT_1:62;
then dom ((F - G) `| X) = dom ((f - g) | X) by A17, FDIFF_1:def 7;
then (F - G) `| X = (f - g) | X by A19, PARTFUN1:5;
hence F - G is_integral_of f - g,X by A17, Lm1; :: thesis: verum