let X be set ; :: thesis: for F, f, G, 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, f, G, 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) + (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) + (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 8;
then (dom g) /\ X = X by RELAT_1:90;
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 8;
then (dom f) /\ X = X by RELAT_1:90;
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

let x be Element of REAL ; :: thesis: ( x in dom ((F (#) G) `| X) implies ((F (#) G) `| X) . x = (((F (#) g) + (f (#) G)) | X) . x )
assume x in dom ((F (#) G) `| X) ; :: thesis: ((F (#) G) `| X) . x = (((F (#) g) + (f (#) G)) | X) . x
then A13: x in X by A9, FDIFF_1:def 8;
then F | X is_differentiable_in x by A8, FDIFF_1:def 7;
then A14: F is_differentiable_in x by A13, Th4;
(G `| X) . x = diff G,x by A3, A13, FDIFF_1:def 8;
then g . x = diff G,x by A5, A13, FUNCT_1:72;
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 8;
then f . x = diff F,x by A10, A13, FUNCT_1:72;
then A16: (f (#) G) . x = (G . x) * (diff F,x) by VALUED_1:5;
G | X is_differentiable_in x by A3, A13, FDIFF_1:def 7;
then A17: G is_differentiable_in x by A13, Th4;
((F (#) G) `| X) . x = diff (F (#) G),x by A9, A13, FDIFF_1:def 8;
then ((F (#) G) `| X) . x = ((G . x) * (diff F,x)) + ((F . x) * (diff G,x)) by A14, A17, FDIFF_1:24;
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:72; :: thesis: verum

end;

X = dom (((f (#) G) + (F (#) g)) | X) by A11, RELAT_1:91;
then dom ((F (#) G) `| X) = dom (((f (#) G) + (F (#) g)) | X) by A9, FDIFF_1:def 8;
then (F (#) G) `| X = ((F (#) g) + (f (#) G)) | X by A12, PARTFUN1:34;
hence F (#) G is_integral_of (f (#) G) + (F (#) g),X by A9, Lm1; :: thesis: verum