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 & c <= d & ['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 & c <= d & ['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 & c <= d & ['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 & c <= d & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) ; :: thesis: integral ((r (#) f),c,d) = r * (integral (f,c,d))
then ['a,b'] = [.a,b.] by INTEGRA5:def 3;
then A2: ( a <= c & c <= b & a <= d & d <= b ) by A1, XXREAL_1:1;
reconsider A = ['c,d'] as non empty closed_interval Subset of REAL ;
( c = min (c,d) & d = max (c,d) ) by A1, XXREAL_0:def 9, XXREAL_0:def 10;
then ['c,d'] c= ['a,b'] by A1, Lm2;
then A4: ( f is_integrable_on A & A c= dom f ) by A1, A2, Th1909;
( integral ((r (#) f),A) = integral ((r (#) f),c,d) & integral (f,A) = integral (f,c,d) ) by A1, INTEGR18:def 9;
hence integral ((r (#) f),c,d) = r * (integral (f,c,d)) by A4, INTEGR18:13; :: thesis: verum