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;

per cases ( r = 0 or r > 0 or r < 0 ) ;

suppose r = 0 ; :: thesis: ( r (#) f is_improper_integrable_on a,b & improper_integral ((r (#) f),a,b) = r * (improper_integral (f,a,b)) )

hence r (#) f is_improper_integrable_on a,b by A3, A7; :: thesis: improper_integral ((r (#) f),a,b) = r * (improper_integral (f,a,b))
hence improper_integral ((r (#) f),a,b) = r * (improper_integral (f,a,b)) by A1, A3, A8, A9, Th48; :: thesis: verum

end;

suppose A10: r > 0 ; :: thesis: ( r (#) f is_improper_integrable_on a,b & improper_integral ((r (#) f),a,b) = r * (improper_integral (f,a,b)) )

A11: now :: thesis: ( left_improper_integral ((r (#) f),a,c) = -infty implies not right_improper_integral ((r (#) f),c,b) = +infty )

assume A12: ( left_improper_integral ((r (#) f),a,c) = -infty & right_improper_integral ((r (#) f),c,b) = +infty ) ; :: thesis: contradiction
then ( left_improper_integral (f,a,c) = +infty or left_improper_integral (f,a,c) = -infty ) by A7, XXREAL_3:70;
hence contradiction by A4, A12, A7, A10, XXREAL_3:69; :: thesis: verum

end;

A13: now :: thesis: ( left_improper_integral ((r (#) f),a,c) = +infty implies not right_improper_integral ((r (#) f),c,b) = -infty )

assume A14: ( left_improper_integral ((r (#) f),a,c) = +infty & right_improper_integral ((r (#) f),c,b) = -infty ) ; :: thesis: contradiction
then ( left_improper_integral (f,a,c) = +infty or left_improper_integral (f,a,c) = -infty ) by A7, XXREAL_3:69;
hence contradiction by A5, A14, A7, A10, XXREAL_3:70; :: thesis: verum

end;

thus r (#) f is_improper_integrable_on a,b by A3, A7, A11, A13; :: thesis: improper_integral ((r (#) f),a,b) = r * (improper_integral (f,a,b))
hence improper_integral ((r (#) f),a,b) = r * (improper_integral (f,a,b)) by A1, A3, A8, A9, Th48; :: thesis: verum

end;

suppose A15: r < 0 ; :: thesis: ( r (#) f is_improper_integrable_on a,b & improper_integral ((r (#) f),a,b) = r * (improper_integral (f,a,b)) )

A16: now :: thesis: ( left_improper_integral ((r (#) f),a,c) = -infty implies not right_improper_integral ((r (#) f),c,b) = +infty )

assume A17: ( left_improper_integral ((r (#) f),a,c) = -infty & right_improper_integral ((r (#) f),c,b) = +infty ) ; :: thesis: contradiction
then ( left_improper_integral (f,a,c) = +infty or left_improper_integral (f,a,c) = -infty ) by A7, XXREAL_3:70;
hence contradiction by A5, A17, A7, A15, XXREAL_3:69; :: thesis: verum

end;

A18: now :: thesis: ( left_improper_integral ((r (#) f),a,c) = +infty implies not right_improper_integral ((r (#) f),c,b) = -infty )

assume A19: ( left_improper_integral ((r (#) f),a,c) = +infty & right_improper_integral ((r (#) f),c,b) = -infty ) ; :: thesis: contradiction
then ( left_improper_integral (f,a,c) = +infty or left_improper_integral (f,a,c) = -infty ) by A7, XXREAL_3:69;
hence contradiction by A4, A19, A7, A15, XXREAL_3:70; :: thesis: verum

end;

thus r (#) f is_improper_integrable_on a,b by A3, A7, A16, A18; :: thesis: improper_integral ((r (#) f),a,b) = r * (improper_integral (f,a,b))
hence improper_integral ((r (#) f),a,b) = r * (improper_integral (f,a,b)) by A1, A3, A8, A9, Th48; :: thesis: verum

end;

end;