let r be real number ; :: 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 F is_integral_of f,X ; :: thesis: r (#) F is_integral_of r (#) f,X
then A1: ( F is_differentiable_on X & F `| X = f | X ) by Lm1;
then A2: r (#) F is_differentiable_on X by Th7;
dom (f | X) = X by A1, FDIFF_1:def 8;
then (dom f) /\ X = X by RELAT_1:90;
then X c= dom f by XBOOLE_1:18;
then A3: X c= dom (r (#) f) by VALUED_1:def 5;
then X = dom ((r (#) f) | X) by RELAT_1:91;
then A4: dom ((r (#) F) `| X) = dom ((r (#) f) | X) by A2, FDIFF_1:def 8;

now

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 A5: x in X by A2, FDIFF_1:def 8;
then A6: ((r (#) F) `| X) . x = diff (r (#) F),x by A2, FDIFF_1:def 8;
reconsider r1 = r as Real by XREAL_0:def 1;
F | X is_differentiable_in x by A1, A5, FDIFF_1:def 7;
then F is_differentiable_in x by A5, Th4;
then A7: ((r1 (#) F) `| X) . x = r1 * (diff F,x) by A6, FDIFF_1:23;
(F `| X) . x = diff F,x by A1, A5, FDIFF_1:def 8;
then f . x = diff F,x by A1, A5, FUNCT_1:72;
then ((r (#) F) `| X) . x = (r (#) f) . x by A3, A5, A7, VALUED_1:def 5;
hence ((r (#) F) `| X) . x = ((r (#) f) | X) . x by A5, FUNCT_1:72; :: thesis: verum

end;

then (r (#) F) `| X = (r (#) f) | X by A4, PARTFUN1:34;
hence r (#) F is_integral_of r (#) f,X by A2, Lm1; :: thesis: verum