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

proof

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

end;

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

suppose A8: f is_right_ext_Riemann_integrable_on a,b ; :: thesis: ( r (#) f is_right_improper_integrable_on a,b & right_improper_integral ((r (#) f),a,b) = r * (right_improper_integral (f,a,b)) )

then A9: right_improper_integral (f,a,b) = ext_right_integral (f,a,b) by A3, Th39;
A10: ( r (#) f is_right_ext_Riemann_integrable_on a,b & ext_right_integral ((r (#) f),a,b) = r * (ext_right_integral (f,a,b)) ) by A2, A8, Th31;
thus r (#) f is_right_improper_integrable_on a,b by A2, A8, Th31, Th33; :: thesis: right_improper_integral ((r (#) f),a,b) = r * (right_improper_integral (f,a,b))
then right_improper_integral ((r (#) f),a,b) = ext_right_integral ((r (#) f),a,b) by A10, Th39;
hence right_improper_integral ((r (#) f),a,b) = r * (right_improper_integral (f,a,b)) by A9, A10, XXREAL_3:def 5; :: thesis: verum

end;

suppose A11: not f is_right_ext_Riemann_integrable_on a,b ; :: thesis: ( r (#) f is_right_improper_integrable_on a,b & right_improper_integral ((r (#) f),a,b) = r * (right_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,a,x) 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),a,x)

proof

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

end;

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

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

then A21: Intf is_left_divergent_to+infty_in b by A3, A12, A13, Th51;

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

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

then A23: r (#) Intf is_left_divergent_to+infty_in b by A20, A3, A12, A13, Th51, LIMFUNC2:21;
thus r (#) f is_right_improper_integrable_on a,b by A4, A14, A15, A22, A21, LIMFUNC2:21; :: thesis: right_improper_integral ((r (#) f),a,b) = r * (right_improper_integral (f,a,b))
then right_improper_integral ((r (#) f),a,b) = +infty by A14, A15, A23, Def4;
hence right_improper_integral ((r (#) f),a,b) = r * (right_improper_integral (f,a,b)) by A20, A22, XXREAL_3:def 5; :: thesis: verum

end;

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

then A25: r (#) Intf is_left_divergent_to-infty_in b by A20, A3, A12, A13, Th51, LIMFUNC2:21;
thus r (#) f is_right_improper_integrable_on a,b by A4, A14, A15, A24, A21, LIMFUNC2:21; :: thesis: right_improper_integral ((r (#) f),a,b) = r * (right_improper_integral (f,a,b))
then right_improper_integral ((r (#) f),a,b) = -infty by A14, A15, A25, Def4;
hence right_improper_integral ((r (#) f),a,b) = r * (right_improper_integral (f,a,b)) by A20, A24, XXREAL_3:def 5; :: thesis: verum

end;

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

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

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

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

end;

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

end;

then A30: r (#) Intf is_left_convergent_in b by A27, LIMFUNC2:7;
then A31: lim_left ((r (#) Intf),b) = 0 by A28, LIMFUNC2:41;
thus r (#) f is_right_improper_integrable_on a,b by A4, A14, A15, A28, A27, LIMFUNC2:7; :: thesis: right_improper_integral ((r (#) f),a,b) = r * (right_improper_integral (f,a,b))
then right_improper_integral ((r (#) f),a,b) = 0 by A14, A15, A30, A31, Def4;
hence right_improper_integral ((r (#) f),a,b) = r * (right_improper_integral (f,a,b)) by A26; :: thesis: verum

end;

end;

end;

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

then A33: Intf is_left_divergent_to-infty_in b by A3, A12, A13, Th52;

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

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

then A35: r (#) Intf is_left_divergent_to-infty_in b by A32, A3, A12, A13, Th52, LIMFUNC2:21;
thus r (#) f is_right_improper_integrable_on a,b by A4, A14, A15, A34, A33, LIMFUNC2:21; :: thesis: right_improper_integral ((r (#) f),a,b) = r * (right_improper_integral (f,a,b))
then right_improper_integral ((r (#) f),a,b) = -infty by A14, A15, A35, Def4;
hence right_improper_integral ((r (#) f),a,b) = r * (right_improper_integral (f,a,b)) by A32, A34, XXREAL_3:def 5; :: thesis: verum

end;

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

then A37: r (#) Intf is_left_divergent_to+infty_in b by A32, A3, A12, A13, Th52, LIMFUNC2:21;
thus r (#) f is_right_improper_integrable_on a,b by A4, A14, A15, A36, A33, LIMFUNC2:21; :: thesis: right_improper_integral ((r (#) f),a,b) = r * (right_improper_integral (f,a,b))
then right_improper_integral ((r (#) f),a,b) = +infty by A14, A15, A37, Def4;
hence right_improper_integral ((r (#) f),a,b) = r * (right_improper_integral (f,a,b)) by A32, A36, XXREAL_3:def 5; :: thesis: verum

end;

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

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

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

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

end;

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

end;

then A42: r (#) Intf is_left_convergent_in b by A39, LIMFUNC2:7;
then A43: lim_left ((r (#) Intf),b) = 0 by A40, LIMFUNC2:41;
thus r (#) f is_right_improper_integrable_on a,b by A4, A14, A15, A40, A39, LIMFUNC2:7; :: thesis: right_improper_integral ((r (#) f),a,b) = r * (right_improper_integral (f,a,b))
then right_improper_integral ((r (#) f),a,b) = 0 by A14, A15, A42, A43, Def4;
hence right_improper_integral ((r (#) f),a,b) = r * (right_improper_integral (f,a,b)) by A38; :: thesis: verum

end;

end;

end;

end;

end;

end;