let f be PartFunc of REAL,REAL; :: thesis: for a, b, r being Real st a < b & ].a,b.] c= dom f & f is_left_improper_integrable_on a,b holds
( r (#) f is_left_improper_integrable_on a,b & left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) )
let a, b, r be Real; :: thesis: ( a < b & ].a,b.] c= dom f & f is_left_improper_integrable_on a,b implies ( r (#) f is_left_improper_integrable_on a,b & left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) ) )
assume that
A1: a < b and
A2: ].a,b.] c= dom f and
A3: f is_left_improper_integrable_on a,b ; :: thesis: ( r (#) f is_left_improper_integrable_on a,b & left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) )
A4: for d being Real st a < d & d <= b holds
( r (#) f is_integrable_on ['d,b'] & (r (#) f) | ['d,b'] is bounded )

proof

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

end;

per cases ( f is_left_ext_Riemann_integrable_on a,b or not f is_left_ext_Riemann_integrable_on a,b ) ;

suppose A8: f is_left_ext_Riemann_integrable_on a,b ; :: thesis: ( r (#) f is_left_improper_integrable_on a,b & left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) )

then A9: left_improper_integral (f,a,b) = ext_left_integral (f,a,b) by A3, Th34;
A10: ( r (#) f is_left_ext_Riemann_integrable_on a,b & ext_left_integral ((r (#) f),a,b) = r * (ext_left_integral (f,a,b)) ) by A2, A8, Th30;
thus r (#) f is_left_improper_integrable_on a,b by A2, A8, Th30, Th32; :: thesis: left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b))
then left_improper_integral ((r (#) f),a,b) = ext_left_integral ((r (#) f),a,b) by A10, Th34;
hence left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) by A9, A10, XXREAL_3:def 5; :: thesis: verum

end;

suppose A11: not f is_left_ext_Riemann_integrable_on a,b ; :: thesis: ( r (#) f is_left_improper_integrable_on a,b & left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) )

consider Intf being PartFunc of REAL,REAL such that
A12: dom Intf = ].a,b.] and
A13: for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) by A3;
A14: dom (r (#) Intf) = ].a,b.] by A12, VALUED_1:def 5;
A15: 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 A16: x in dom (r (#) Intf) ; :: thesis: (r (#) Intf) . x = integral ((r (#) f),x,b)
then A17: (r (#) Intf) . x = r * (Intf . x) by VALUED_1:def 5
.= r * (integral (f,x,b)) by A16, A14, A13, A12 ;
A18: ( a < x & x <= b ) by A14, A16, XXREAL_1:2;
then [.x,b.] c= ].a,b.] by XXREAL_1:39;
then [.x,b.] c= dom f by A2;
then A19: ['x,b'] c= dom f by A18, INTEGRA5:def 3;
( f is_integrable_on ['x,b'] & f | ['x,b'] is bounded ) by A3, A18;
hence (r (#) Intf) . x = integral ((r (#) f),x,b) by A17, A18, A19, INTEGRA6:10; :: thesis: verum

end;

per cases ( left_improper_integral (f,a,b) = +infty or left_improper_integral (f,a,b) = -infty ) by A3, A11, Th34;

suppose A20: left_improper_integral (f,a,b) = +infty ; :: thesis: ( r (#) f is_left_improper_integrable_on a,b & left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) )

then A21: Intf is_right_divergent_to+infty_in a by A3, A12, A13, Th49;

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

suppose A22: r > 0 ; :: thesis: ( r (#) f is_left_improper_integrable_on a,b & left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) )

then A23: r (#) Intf is_right_divergent_to+infty_in a by A20, A3, A12, A13, Th49, LIMFUNC2:22;
thus r (#) f is_left_improper_integrable_on a,b by A4, A14, A15, A22, A21, LIMFUNC2:22; :: thesis: left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b))
then left_improper_integral ((r (#) f),a,b) = +infty by A14, A15, A23, Def3;
hence left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) by A20, A22, XXREAL_3:def 5; :: thesis: verum

end;

suppose A24: r < 0 ; :: thesis: ( r (#) f is_left_improper_integrable_on a,b & left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) )

then A25: r (#) Intf is_right_divergent_to-infty_in a by A20, A3, A12, A13, Th49, LIMFUNC2:22;
thus r (#) f is_left_improper_integrable_on a,b by A4, A14, A15, A24, A21, LIMFUNC2:22; :: thesis: left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b))
then left_improper_integral ((r (#) f),a,b) = -infty by A14, A15, A25, Def3;
hence left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) by A20, A24, XXREAL_3:def 5; :: thesis: verum

end;

suppose A26: r = 0 ; :: thesis: ( r (#) f is_left_improper_integrable_on a,b & left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) )

A27: for R being Real st a < R holds
ex g being Real st
( g < R & a < g & g in dom (r (#) Intf) ) by A12, A14, A21, LIMFUNC2:11;
A28: for g1 being Real st 0 < g1 holds
ex R being Real st
( a < R & ( for r1 being Real st r1 < R & a < r1 & 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
( a < R & ( for r1 being Real st r1 < R & a < r1 & r1 in dom (r (#) Intf) holds
|.(((r (#) Intf) . r1) - 0).| < g1 ) ) )
assume A29: 0 < g1 ; :: thesis: ex R being Real st
( a < R & ( for r1 being Real st r1 < R & a < r1 & r1 in dom (r (#) Intf) holds
|.(((r (#) Intf) . r1) - 0).| < g1 ) )

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

let r1 be Real; :: thesis: ( r1 < b & a < r1 & r1 in dom (r (#) Intf) implies |.(((r (#) Intf) . r1) - 0).| < g1 )
assume ( r1 < b & a < r1 & 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 A26 ;
hence |.(((r (#) Intf) . r1) - 0).| < g1 by A29, ABSVALUE:2; :: thesis: verum

end;

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

end;

then A30: r (#) Intf is_right_convergent_in a by A27, LIMFUNC2:10;
then A31: lim_right ((r (#) Intf),a) = 0 by A28, LIMFUNC2:42;
thus r (#) f is_left_improper_integrable_on a,b by A4, A14, A15, A28, A27, LIMFUNC2:10; :: thesis: left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b))
then left_improper_integral ((r (#) f),a,b) = 0 by A14, A15, A30, A31, Def3;
hence left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) by A26; :: thesis: verum

end;

end;

end;

suppose A32: left_improper_integral (f,a,b) = -infty ; :: thesis: ( r (#) f is_left_improper_integrable_on a,b & left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) )

then A33: Intf is_right_divergent_to-infty_in a by A3, A12, A13, Th50;

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

suppose A34: r > 0 ; :: thesis: ( r (#) f is_left_improper_integrable_on a,b & left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) )

then A35: r (#) Intf is_right_divergent_to-infty_in a by A32, A3, A12, A13, Th50, LIMFUNC2:22;
thus r (#) f is_left_improper_integrable_on a,b by A4, A14, A15, A34, A33, LIMFUNC2:22; :: thesis: left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b))
then left_improper_integral ((r (#) f),a,b) = -infty by A14, A15, A35, Def3;
hence left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) by A32, A34, XXREAL_3:def 5; :: thesis: verum

end;

suppose A36: r < 0 ; :: thesis: ( r (#) f is_left_improper_integrable_on a,b & left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) )

then A37: r (#) Intf is_right_divergent_to+infty_in a by A32, A3, A12, A13, Th50, LIMFUNC2:22;
thus r (#) f is_left_improper_integrable_on a,b by A4, A14, A15, A36, A33, LIMFUNC2:22; :: thesis: left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b))
then left_improper_integral ((r (#) f),a,b) = +infty by A14, A15, A37, Def3;
hence left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) by A32, A36, XXREAL_3:def 5; :: thesis: verum

end;

suppose A38: r = 0 ; :: thesis: ( r (#) f is_left_improper_integrable_on a,b & left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) )

A39: for R being Real st a < R holds
ex g being Real st
( g < R & a < g & g in dom (r (#) Intf) ) by A12, A14, A33, LIMFUNC2:12;
A40: for g1 being Real st 0 < g1 holds
ex R being Real st
( a < R & ( for r1 being Real st r1 < R & a < r1 & 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
( a < R & ( for r1 being Real st r1 < R & a < r1 & r1 in dom (r (#) Intf) holds
|.(((r (#) Intf) . r1) - 0).| < g1 ) ) )
assume A41: 0 < g1 ; :: thesis: ex R being Real st
( a < R & ( for r1 being Real st r1 < R & a < r1 & r1 in dom (r (#) Intf) holds
|.(((r (#) Intf) . r1) - 0).| < g1 ) )

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

let r1 be Real; :: thesis: ( r1 < b & a < r1 & r1 in dom (r (#) Intf) implies |.(((r (#) Intf) . r1) - 0).| < g1 )
assume ( r1 < b & a < r1 & 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 A38 ;
hence |.(((r (#) Intf) . r1) - 0).| < g1 by A41, ABSVALUE:2; :: thesis: verum

end;

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

end;

then A42: r (#) Intf is_right_convergent_in a by A39, LIMFUNC2:10;
then A43: lim_right ((r (#) Intf),a) = 0 by A40, LIMFUNC2:42;
thus r (#) f is_left_improper_integrable_on a,b by A4, A14, A15, A40, A39, LIMFUNC2:10; :: thesis: left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b))
then left_improper_integral ((r (#) f),a,b) = 0 by A14, A15, A42, A43, Def3;
hence left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) by A38; :: thesis: verum

end;

end;

end;

end;

end;

end;