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) + (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) + (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) + (F (#) g),X
A3:
G is_differentiable_on X
by A2, Lm1;
A4:
X c= dom F
by A1, Th11;
A5:
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
X c= dom g
by XBOOLE_1:18;
then
X c= (dom F) /\ (dom g)
by A4, XBOOLE_1:19;
then A6:
X c= dom (F (#) g)
by VALUED_1:def 4;
A7:
X c= dom G
by A2, Th11;
A8:
F is_differentiable_on X
by A1, Lm1;
then A9:
F (#) G is_differentiable_on X
by A3, Th6;
A10:
F `| X = f | X
by A1, Lm1;
then
dom (f | X) = X
by A8, FDIFF_1:def 7;
then
(dom f) /\ X = X
by RELAT_1:61;
then
X c= dom f
by XBOOLE_1:18;
then
X c= (dom f) /\ (dom G)
by A7, XBOOLE_1:19;
then
X c= dom (f (#) G)
by VALUED_1:def 4;
then
X c= (dom (f (#) G)) /\ (dom (F (#) g))
by A6, XBOOLE_1:19;
then A11:
X c= dom ((f (#) G) + (F (#) g))
by VALUED_1:def 1;
A12:
now for x being Element of REAL st x in dom ((F (#) G) `| X) holds
((F (#) G) `| X) . x = (((F (#) g) + (f (#) G)) | X) . xlet x be
Element of
REAL ;
( x in dom ((F (#) G) `| X) implies ((F (#) G) `| X) . x = (((F (#) g) + (f (#) G)) | X) . x )assume
x in dom ((F (#) G) `| X)
;
((F (#) G) `| X) . x = (((F (#) g) + (f (#) G)) | X) . xthen A13:
x in X
by A9, FDIFF_1:def 7;
then
F | X is_differentiable_in x
by A8;
then A14:
F is_differentiable_in x
by A13, Th4;
(G `| X) . x = diff (
G,
x)
by A3, A13, FDIFF_1:def 7;
then
g . x = diff (
G,
x)
by A5, A13, FUNCT_1:49;
then A15:
(F (#) g) . x = (F . x) * (diff (G,x))
by VALUED_1:5;
(F `| X) . x = diff (
F,
x)
by A8, A13, FDIFF_1:def 7;
then
f . x = diff (
F,
x)
by A10, A13, FUNCT_1:49;
then A16:
(f (#) G) . x = (G . x) * (diff (F,x))
by VALUED_1:5;
G | X is_differentiable_in x
by A3, A13;
then A17:
G is_differentiable_in x
by A13, Th4;
((F (#) G) `| X) . x = diff (
(F (#) G),
x)
by A9, A13, FDIFF_1:def 7;
then
((F (#) G) `| X) . x = ((G . x) * (diff (F,x))) + ((F . x) * (diff (G,x)))
by A14, A17, FDIFF_1:16;
then
((F (#) G) `| X) . x = ((F (#) g) + (f (#) G)) . x
by A11, A13, A15, A16, VALUED_1:def 1;
hence
((F (#) G) `| X) . x = (((F (#) g) + (f (#) G)) | X) . x
by A13, FUNCT_1:49;
verum end;
X = dom (((f (#) G) + (F (#) g)) | X)
by A11, RELAT_1:62;
then
dom ((F (#) G) `| X) = dom (((f (#) G) + (F (#) g)) | X)
by A9, FDIFF_1:def 7;
then
(F (#) G) `| X = ((F (#) g) + (f (#) G)) | X
by A12, PARTFUN1:5;
hence
F (#) G is_integral_of (f (#) G) + (F (#) g),X
by A9, Lm1; verum