let X be set ; 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; ( 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
; ( 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 for x being Element of REAL st x in dom ((F + G) `| X) holds
((F + G) `| X) . x = ((f + g) | X) . xlet x be
Element of
REAL ;
( x in dom ((F + G) `| X) implies ((F + G) `| X) . x = ((f + g) | X) . x )assume
x in dom ((F + G) `| X)
;
((F + G) `| X) . x = ((f + g) | X) . xthen 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;
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 for x being Element of REAL st x in dom ((F - G) `| X) holds
((F - G) `| X) . x = ((f - g) | X) . xlet x be
Element of
REAL ;
( x in dom ((F - G) `| X) implies ((F - G) `| X) . x = ((f - g) | X) . x )assume
x in dom ((F - G) `| X)
;
((F - G) `| X) . x = ((f - g) | X) . xthen 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;
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; 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; verum