let f be PartFunc of REAL,REAL; :: thesis: for a, b, r being Real st ].a,b.[ c= dom f & f is_improper_integrable_on a,b holds
( r (#) f is_improper_integrable_on a,b & improper_integral ((r (#) f),a,b) = r * (improper_integral (f,a,b)) )
let a, b, r be Real; :: thesis: ( ].a,b.[ c= dom f & f is_improper_integrable_on a,b implies ( r (#) f is_improper_integrable_on a,b & improper_integral ((r (#) f),a,b) = r * (improper_integral (f,a,b)) ) )
assume that
A1: ].a,b.[ c= dom f and
A2: f is_improper_integrable_on a,b ; :: thesis: ( r (#) f is_improper_integrable_on a,b & improper_integral ((r (#) f),a,b) = r * (improper_integral (f,a,b)) )
consider c being Real such that
A3: ( a < c & c < b ) and
f is_left_improper_integrable_on a,c and
f is_right_improper_integrable_on c,b and
A4: ( not left_improper_integral (f,a,c) = -infty or not right_improper_integral (f,c,b) = +infty ) and
A5: ( not left_improper_integral (f,a,c) = +infty or not right_improper_integral (f,c,b) = -infty ) by A2;
( ].a,c.] c= ].a,b.[ & [.c,b.[ c= ].a,b.[ ) by A3, XXREAL_1:48, XXREAL_1:49;
then A6: ( ].a,c.] c= dom f & [.c,b.[ c= dom f ) by A1;
( f is_left_improper_integrable_on a,c & f is_right_improper_integrable_on c,b ) by A1, A2, A3, Th48;
then A7: ( r (#) f is_left_improper_integrable_on a,c & r (#) f is_right_improper_integrable_on c,b & left_improper_integral ((r (#) f),a,c) = r * (left_improper_integral (f,a,c)) & right_improper_integral ((r (#) f),c,b) = r * (right_improper_integral (f,c,b)) ) by A3, A6, Th53, Th54;
A8: (left_improper_integral ((r (#) f),a,c)) + (right_improper_integral ((r (#) f),c,b)) = r * ((left_improper_integral (f,a,c)) + (right_improper_integral (f,c,b))) by A7, XXREAL_3:95
.= r * (improper_integral (f,a,b)) by A1, A2, A3, Th48 ;
A9: dom (r (#) f) = dom f by VALUED_1:def 5;