let r be Real; :: thesis: for X being set
for f, F being PartFunc of REAL,REAL st F is_integral_of f,X holds
r (#) F is_integral_of r (#) f,X
let X be set ; :: thesis: for f, F being PartFunc of REAL,REAL st F is_integral_of f,X holds
r (#) F is_integral_of r (#) f,X
let f, F be PartFunc of REAL,REAL; :: thesis: ( F is_integral_of f,X implies r (#) F is_integral_of r (#) f,X )
assume A1: F is_integral_of f,X ; :: thesis: r (#) F is_integral_of r (#) f,X
then A2: F is_differentiable_on X by Lm1;
then A3: r (#) F is_differentiable_on X by Th7;
A4: F `| X = f | X by A1, Lm1;
then dom (f | X) = X by A2, FDIFF_1:def 7;
then (dom f) /\ X = X by RELAT_1:61;
then X c= dom f by XBOOLE_1:18;
then A5: X c= dom (r (#) f) by VALUED_1:def 5;

A6: now :: thesis: for x being Element of REAL st x in dom ((r (#) F) `| X) holds
((r (#) F) `| X) . x = ((r (#) f) | X) . x

reconsider r1 = r as Real ;
let x be Element of REAL ; :: thesis: ( x in dom ((r (#) F) `| X) implies ((r (#) F) `| X) . x = ((r (#) f) | X) . x )
assume x in dom ((r (#) F) `| X) ; :: thesis: ((r (#) F) `| X) . x = ((r (#) f) | X) . x
then A7: x in X by A3, FDIFF_1:def 7;
then F | X is_differentiable_in x by A2;
then A8: F is_differentiable_in x by A7, Th4;
((r (#) F) `| X) . x = diff ((r (#) F),x) by A3, A7, FDIFF_1:def 7;
then A9: ((r1 (#) F) `| X) . x = r1 * (diff (F,x)) by A8, FDIFF_1:15;
(F `| X) . x = diff (F,x) by A2, A7, FDIFF_1:def 7;
then f . x = diff (F,x) by A4, A7, FUNCT_1:49;
then ((r (#) F) `| X) . x = (r (#) f) . x by A5, A7, A9, VALUED_1:def 5;
hence ((r (#) F) `| X) . x = ((r (#) f) | X) . x by A7, FUNCT_1:49; :: thesis: verum

end;

X = dom ((r (#) f) | X) by A5, RELAT_1:62;
then dom ((r (#) F) `| X) = dom ((r (#) f) | X) by A3, FDIFF_1:def 7;
then (r (#) F) `| X = (r (#) f) | X by A6, PARTFUN1:5;
hence r (#) F is_integral_of r (#) f,X by A3, Lm1; :: thesis: verum