let f be PartFunc of REAL,REAL; :: thesis: for r being Real st dom f = REAL & f is_improper_integrable_on_REAL holds
( r (#) f is_improper_integrable_on_REAL & improper_integral_on_REAL (r (#) f) = r * (improper_integral_on_REAL f) )
let r be Real; :: thesis: ( dom f = REAL & f is_improper_integrable_on_REAL implies ( r (#) f is_improper_integrable_on_REAL & improper_integral_on_REAL (r (#) f) = r * (improper_integral_on_REAL f) ) )
assume that
A1: dom f = REAL and
A2: f is_improper_integrable_on_REAL ; :: thesis: ( r (#) f is_improper_integrable_on_REAL & improper_integral_on_REAL (r (#) f) = r * (improper_integral_on_REAL f) )
consider c being Real such that
f is_-infty_improper_integrable_on c and
f is_+infty_improper_integrable_on c and
A3: ( not improper_integral_-infty (f,c) = -infty or not improper_integral_+infty (f,c) = +infty ) and
A4: ( not improper_integral_-infty (f,c) = +infty or not improper_integral_+infty (f,c) = -infty ) by A2;
( f is_-infty_improper_integrable_on c & f is_+infty_improper_integrable_on c ) by A1, A2, Th36;
then A5: ( r (#) f is_-infty_improper_integrable_on c & r (#) f is_+infty_improper_integrable_on c & improper_integral_-infty ((r (#) f),c) = r * (improper_integral_-infty (f,c)) & improper_integral_+infty ((r (#) f),c) = r * (improper_integral_+infty (f,c)) ) by A1, Th41, Th42;
A6: (improper_integral_-infty ((r (#) f),c)) + (improper_integral_+infty ((r (#) f),c)) = r * ((improper_integral_-infty (f,c)) + (improper_integral_+infty (f,c))) by A5, XXREAL_3:95
.= r * (improper_integral_on_REAL f) by A1, A2, Th36 ;
A7: 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_REAL & improper_integral_on_REAL (r (#) f) = r * (improper_integral_on_REAL f) )

hence r (#) f is_improper_integrable_on_REAL by A5; :: thesis: improper_integral_on_REAL (r (#) f) = r * (improper_integral_on_REAL f)
hence improper_integral_on_REAL (r (#) f) = r * (improper_integral_on_REAL f) by A1, A6, A7, Th36; :: thesis: verum

end;

suppose A8: r > 0 ; :: thesis: ( r (#) f is_improper_integrable_on_REAL & improper_integral_on_REAL (r (#) f) = r * (improper_integral_on_REAL f) )

A9: now :: thesis: ( improper_integral_-infty ((r (#) f),c) = -infty implies not improper_integral_+infty ((r (#) f),c) = +infty )

assume A10: ( improper_integral_-infty ((r (#) f),c) = -infty & improper_integral_+infty ((r (#) f),c) = +infty ) ; :: thesis: contradiction
then ( improper_integral_-infty (f,c) = +infty or improper_integral_-infty (f,c) = -infty ) by A5, XXREAL_3:70;
hence contradiction by A3, A10, A5, A8, XXREAL_3:69; :: thesis: verum

end;

A11: now :: thesis: ( improper_integral_-infty ((r (#) f),c) = +infty implies not improper_integral_+infty ((r (#) f),c) = -infty )

assume A12: ( improper_integral_-infty ((r (#) f),c) = +infty & improper_integral_+infty ((r (#) f),c) = -infty ) ; :: thesis: contradiction
then ( improper_integral_-infty (f,c) = +infty or improper_integral_-infty (f,c) = -infty ) by A5, XXREAL_3:69;
hence contradiction by A4, A12, A5, A8, XXREAL_3:70; :: thesis: verum

end;

thus r (#) f is_improper_integrable_on_REAL by A5, A9, A11; :: thesis: improper_integral_on_REAL (r (#) f) = r * (improper_integral_on_REAL f)
hence improper_integral_on_REAL (r (#) f) = r * (improper_integral_on_REAL f) by A1, A6, A7, Th36; :: thesis: verum

end;

suppose A13: r < 0 ; :: thesis: ( r (#) f is_improper_integrable_on_REAL & improper_integral_on_REAL (r (#) f) = r * (improper_integral_on_REAL f) )

A14: now :: thesis: ( improper_integral_-infty ((r (#) f),c) = -infty implies not improper_integral_+infty ((r (#) f),c) = +infty )

assume A15: ( improper_integral_-infty ((r (#) f),c) = -infty & improper_integral_+infty ((r (#) f),c) = +infty ) ; :: thesis: contradiction
then ( improper_integral_-infty (f,c) = +infty or improper_integral_-infty (f,c) = -infty ) by A5, XXREAL_3:70;
hence contradiction by A4, A15, A5, A13, XXREAL_3:69; :: thesis: verum

end;

A16: now :: thesis: ( improper_integral_-infty ((r (#) f),c) = +infty implies not improper_integral_+infty ((r (#) f),c) = -infty )

assume A17: ( improper_integral_-infty ((r (#) f),c) = +infty & improper_integral_+infty ((r (#) f),c) = -infty ) ; :: thesis: contradiction
then ( improper_integral_-infty (f,c) = +infty or improper_integral_-infty (f,c) = -infty ) by A5, XXREAL_3:69;
hence contradiction by A3, A17, A5, A13, XXREAL_3:70; :: thesis: verum

end;

thus r (#) f is_improper_integrable_on_REAL by A5, A14, A16; :: thesis: improper_integral_on_REAL (r (#) f) = r * (improper_integral_on_REAL f)
hence improper_integral_on_REAL (r (#) f) = r * (improper_integral_on_REAL f) by A1, A6, A7, Th36; :: thesis: verum

end;

end;