let a, b, c, d, r be Real; :: thesis: for Y being RealBanachSpace
for f being continuous PartFunc of REAL, the carrier of Y st a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral ((r (#) f),c,d) = r * (integral (f,c,d))
let Y be RealBanachSpace; :: thesis: for f being continuous PartFunc of REAL, the carrier of Y st a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral ((r (#) f),c,d) = r * (integral (f,c,d))
let f be continuous PartFunc of REAL, the carrier of Y; :: thesis: ( a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies integral ((r (#) f),c,d) = r * (integral (f,c,d)) )
assume A1: ( a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) ; :: thesis: integral ((r (#) f),c,d) = r * (integral (f,c,d))

per cases ( not c <= d or c <= d ) ;

suppose A2: not c <= d ; :: thesis: integral ((r (#) f),c,d) = r * (integral (f,c,d))

reconsider A = ['d,c'] as non empty closed_interval Subset of REAL ;
( d = min (c,d) & c = max (c,d) ) by A2, XXREAL_0:def 9, XXREAL_0:def 10;
then ['d,c'] c= ['a,b'] by A1, Lm2;
then A7: A c= dom f by A1;
then A c= dom (r (#) f) by VFUNCT_1:def 4;
then A8: ( - (integral ((r (#) f),d,c)) = integral ((r (#) f),c,d) & - (integral (f,d,c)) = integral (f,c,d) ) by A2, A7, Th1947;
integral ((r (#) f),d,c) = r * (integral (f,d,c)) by A1, A2, Th1925a;
hence integral ((r (#) f),c,d) = r * (integral (f,c,d)) by A8, RLVECT_1:25; :: thesis: verum

end;

suppose c <= d ; :: thesis: integral ((r (#) f),c,d) = r * (integral (f,c,d))

hence integral ((r (#) f),c,d) = r * (integral (f,c,d)) by A1, Th1925a; :: thesis: verum

end;

end;