let f be PartFunc of REAL,REAL; :: thesis: for b, r being Real st left_closed_halfline b c= dom f & f is_-infty_improper_integrable_on b holds
( r (#) f is_-infty_improper_integrable_on b & improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b)) )
let b, r be Real; :: thesis: ( left_closed_halfline b c= dom f & f is_-infty_improper_integrable_on b implies ( r (#) f is_-infty_improper_integrable_on b & improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b)) ) )
assume that
A1: left_closed_halfline b c= dom f and
A2: f is_-infty_improper_integrable_on b ; :: thesis: ( r (#) f is_-infty_improper_integrable_on b & improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b)) )
A3: for d being Real st d <= b holds
( r (#) f is_integrable_on ['d,b'] & (r (#) f) | ['d,b'] is bounded )

proof

let d be Real; :: thesis: ( d <= b implies ( r (#) f is_integrable_on ['d,b'] & (r (#) f) | ['d,b'] is bounded ) )
assume A4: d <= b ; :: thesis: ( r (#) f is_integrable_on ['d,b'] & (r (#) f) | ['d,b'] is bounded )
[.d,b.] c= ].-infty,b.] by XXREAL_1:265;
then [.d,b.] c= dom f by A1;
then A5: ['d,b'] c= dom f by A4, INTEGRA5:def 3;
A6: ( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) by A2, A4;
hence r (#) f is_integrable_on ['d,b'] by A5, INTEGRA6:9; :: thesis: (r (#) f) | ['d,b'] is bounded
thus (r (#) f) | ['d,b'] is bounded by A6, RFUNCT_1:80; :: thesis: verum

end;

per cases ( f is_-infty_ext_Riemann_integrable_on b or not f is_-infty_ext_Riemann_integrable_on b ) ;

suppose A7: f is_-infty_ext_Riemann_integrable_on b ; :: thesis: ( r (#) f is_-infty_improper_integrable_on b & improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b)) )

then A8: improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) by A2, Th22;
A9: ( r (#) f is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral ((r (#) f),b) = r * (infty_ext_left_integral (f,b)) ) by A1, A7, INTEGR10:11;
thus r (#) f is_-infty_improper_integrable_on b by A1, A7, INTEGR10:11, Th20; :: thesis: improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b))
then improper_integral_-infty ((r (#) f),b) = infty_ext_left_integral ((r (#) f),b) by A9, Th22;
hence improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b)) by A8, A9, XXREAL_3:def 5; :: thesis: verum

end;

suppose A10: not f is_-infty_ext_Riemann_integrable_on b ; :: thesis: ( r (#) f is_-infty_improper_integrable_on b & improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b)) )

consider Intf being PartFunc of REAL,REAL such that
A11: dom Intf = left_closed_halfline b and
A12: for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) by A2;
A13: dom (r (#) Intf) = left_closed_halfline b by A11, VALUED_1:def 5;
A14: for x being Real st x in dom (r (#) Intf) holds
(r (#) Intf) . x = integral ((r (#) f),x,b)

proof

let x be Real; :: thesis: ( x in dom (r (#) Intf) implies (r (#) Intf) . x = integral ((r (#) f),x,b) )
assume A15: x in dom (r (#) Intf) ; :: thesis: (r (#) Intf) . x = integral ((r (#) f),x,b)
then A16: (r (#) Intf) . x = r * (Intf . x) by VALUED_1:def 5
.= r * (integral (f,x,b)) by A15, A13, A12, A11 ;
A17: x <= b by A13, A15, XXREAL_1:2;
[.x,b.] c= ].-infty,b.] by XXREAL_1:265;
then [.x,b.] c= dom f by A1;
then A18: ['x,b'] c= dom f by A17, INTEGRA5:def 3;
( f is_integrable_on ['x,b'] & f | ['x,b'] is bounded ) by A2, A17;
hence (r (#) Intf) . x = integral ((r (#) f),x,b) by A16, A17, A18, INTEGRA6:10; :: thesis: verum

end;

per cases ( improper_integral_-infty (f,b) = +infty or improper_integral_-infty (f,b) = -infty ) by A2, A10, Th22;

suppose A19: improper_integral_-infty (f,b) = +infty ; :: thesis: ( r (#) f is_-infty_improper_integrable_on b & improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b)) )

then A20: Intf is divergent_in-infty_to+infty by A2, A11, A12, Th37;

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

suppose A21: r > 0 ; :: thesis: ( r (#) f is_-infty_improper_integrable_on b & improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b)) )

then A22: r (#) Intf is divergent_in-infty_to+infty by A19, A2, A11, A12, Th37, LIMFUNC1:59;
thus r (#) f is_-infty_improper_integrable_on b by A3, A13, A14, A21, A20, LIMFUNC1:59; :: thesis: improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b))
then improper_integral_-infty ((r (#) f),b) = +infty by A13, A14, A22, Def3;
hence improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b)) by A19, A21, XXREAL_3:def 5; :: thesis: verum

end;

suppose A23: r < 0 ; :: thesis: ( r (#) f is_-infty_improper_integrable_on b & improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b)) )

then A24: r (#) Intf is divergent_in-infty_to-infty by A19, A2, A11, A12, Th37, LIMFUNC1:59;
thus r (#) f is_-infty_improper_integrable_on b by A3, A13, A14, A23, A20, LIMFUNC1:59; :: thesis: improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b))
then improper_integral_-infty ((r (#) f),b) = -infty by A13, A14, A24, Def3;
hence improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b)) by A19, A23, XXREAL_3:def 5; :: thesis: verum

end;

suppose A25: r = 0 ; :: thesis: ( r (#) f is_-infty_improper_integrable_on b & improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b)) )

A26: for R being Real ex g being Real st
( g < R & g in dom (r (#) Intf) ) by A11, A13, A20, LIMFUNC1:48;
A27: for g1 being Real st 0 < g1 holds
ex R being Real st
for r1 being Real st r1 < R & r1 in dom (r (#) Intf) holds
|.(((r (#) Intf) . r1) - 0).| < g1

proof

let g1 be Real; :: thesis: ( 0 < g1 implies ex R being Real st
for r1 being Real st r1 < R & r1 in dom (r (#) Intf) holds
|.(((r (#) Intf) . r1) - 0).| < g1 )
assume A28: 0 < g1 ; :: thesis: ex R being Real st
for r1 being Real st r1 < R & r1 in dom (r (#) Intf) holds
|.(((r (#) Intf) . r1) - 0).| < g1

now :: thesis: for r1 being Real st r1 < b & r1 in dom (r (#) Intf) holds
|.(((r (#) Intf) . r1) - 0).| < g1

let r1 be Real; :: thesis: ( r1 < b & r1 in dom (r (#) Intf) implies |.(((r (#) Intf) . r1) - 0).| < g1 )
assume ( r1 < b & r1 in dom (r (#) Intf) ) ; :: thesis: |.(((r (#) Intf) . r1) - 0).| < g1
then (r (#) Intf) . r1 = r * (Intf . r1) by VALUED_1:def 5
.= 0 by A25 ;
hence |.(((r (#) Intf) . r1) - 0).| < g1 by A28, ABSVALUE:2; :: thesis: verum

end;

hence ex R being Real st
for r1 being Real st r1 < R & r1 in dom (r (#) Intf) holds
|.(((r (#) Intf) . r1) - 0).| < g1 ; :: thesis: verum

end;

then A29: r (#) Intf is convergent_in-infty by A26, LIMFUNC1:45;
then A30: lim_in-infty (r (#) Intf) = 0 by A27, LIMFUNC1:78;
thus r (#) f is_-infty_improper_integrable_on b by A3, A13, A14, A27, A26, LIMFUNC1:45; :: thesis: improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b))
then improper_integral_-infty ((r (#) f),b) = 0 by A13, A14, A29, A30, Def3;
hence improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b)) by A25; :: thesis: verum

end;

end;

end;

suppose A31: improper_integral_-infty (f,b) = -infty ; :: thesis: ( r (#) f is_-infty_improper_integrable_on b & improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b)) )

then A32: Intf is divergent_in-infty_to-infty by A2, A11, A12, Th38;

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

suppose A33: r > 0 ; :: thesis: ( r (#) f is_-infty_improper_integrable_on b & improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b)) )

then A34: r (#) Intf is divergent_in-infty_to-infty by A31, A2, A11, A12, Th38, LIMFUNC1:59;
thus r (#) f is_-infty_improper_integrable_on b by A3, A13, A14, A33, A32, LIMFUNC1:59; :: thesis: improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b))
then improper_integral_-infty ((r (#) f),b) = -infty by A13, A14, A34, Def3;
hence improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b)) by A31, A33, XXREAL_3:def 5; :: thesis: verum

end;

suppose A35: r < 0 ; :: thesis: ( r (#) f is_-infty_improper_integrable_on b & improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b)) )

then A36: r (#) Intf is divergent_in-infty_to+infty by A31, A2, A11, A12, Th38, LIMFUNC1:59;
thus r (#) f is_-infty_improper_integrable_on b by A3, A13, A14, A35, A32, LIMFUNC1:59; :: thesis: improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b))
then improper_integral_-infty ((r (#) f),b) = +infty by A13, A14, A36, Def3;
hence improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b)) by A31, A35, XXREAL_3:def 5; :: thesis: verum

end;

suppose A37: r = 0 ; :: thesis: ( r (#) f is_-infty_improper_integrable_on b & improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b)) )

A38: for R being Real ex g being Real st
( g < R & g in dom (r (#) Intf) ) by A11, A13, A32, LIMFUNC1:49;
A39: for g1 being Real st 0 < g1 holds
ex R being Real st
for r1 being Real st r1 < R & r1 in dom (r (#) Intf) holds
|.(((r (#) Intf) . r1) - 0).| < g1

proof

let g1 be Real; :: thesis: ( 0 < g1 implies ex R being Real st
for r1 being Real st r1 < R & r1 in dom (r (#) Intf) holds
|.(((r (#) Intf) . r1) - 0).| < g1 )
assume A40: 0 < g1 ; :: thesis: ex R being Real st
for r1 being Real st r1 < R & r1 in dom (r (#) Intf) holds
|.(((r (#) Intf) . r1) - 0).| < g1

now :: thesis: for r1 being Real st r1 < b & r1 in dom (r (#) Intf) holds
|.(((r (#) Intf) . r1) - 0).| < g1

let r1 be Real; :: thesis: ( r1 < b & r1 in dom (r (#) Intf) implies |.(((r (#) Intf) . r1) - 0).| < g1 )
assume ( r1 < b & r1 in dom (r (#) Intf) ) ; :: thesis: |.(((r (#) Intf) . r1) - 0).| < g1
then (r (#) Intf) . r1 = r * (Intf . r1) by VALUED_1:def 5
.= 0 by A37 ;
hence |.(((r (#) Intf) . r1) - 0).| < g1 by A40, ABSVALUE:2; :: thesis: verum

end;

hence ex R being Real st
for r1 being Real st r1 < R & r1 in dom (r (#) Intf) holds
|.(((r (#) Intf) . r1) - 0).| < g1 ; :: thesis: verum

end;

then A41: r (#) Intf is convergent_in-infty by A38, LIMFUNC1:45;
then A42: lim_in-infty (r (#) Intf) = 0 by A39, LIMFUNC1:78;
thus r (#) f is_-infty_improper_integrable_on b by A3, A13, A14, A39, A38, LIMFUNC1:45; :: thesis: improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b))
then improper_integral_-infty ((r (#) f),b) = 0 by A13, A14, A41, A42, Def3;
hence improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b)) by A37; :: thesis: verum

end;

end;

end;

end;

end;

end;