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

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

suppose f is_left_ext_Riemann_integrable_on a,b ; :: thesis: ( f is_left_improper_integrable_on a,c & ( left_improper_integral (f,a,b) = ext_left_integral (f,a,b) implies left_improper_integral (f,a,c) = (left_improper_integral (f,a,b)) + (integral (f,b,c)) ) & ( left_improper_integral (f,a,b) = +infty implies left_improper_integral (f,a,c) = +infty ) & ( left_improper_integral (f,a,b) = -infty implies left_improper_integral (f,a,c) = -infty ) )

then left_improper_integral (f,a,b) = ext_left_integral (f,a,b) by A4, Th34;
hence ( f is_left_improper_integrable_on a,c & ( left_improper_integral (f,a,b) = ext_left_integral (f,a,b) implies left_improper_integral (f,a,c) = (left_improper_integral (f,a,b)) + (integral (f,b,c)) ) & ( left_improper_integral (f,a,b) = +infty implies left_improper_integral (f,a,c) = +infty ) & ( left_improper_integral (f,a,b) = -infty implies left_improper_integral (f,a,c) = -infty ) ) by A1, A2, A3, A4, A5, Lm12; :: thesis: verum

end;

suppose not f is_left_ext_Riemann_integrable_on a,b ; :: thesis: ( f is_left_improper_integrable_on a,c & ( left_improper_integral (f,a,b) = ext_left_integral (f,a,b) implies left_improper_integral (f,a,c) = (left_improper_integral (f,a,b)) + (integral (f,b,c)) ) & ( left_improper_integral (f,a,b) = +infty implies left_improper_integral (f,a,c) = +infty ) & ( left_improper_integral (f,a,b) = -infty implies left_improper_integral (f,a,c) = -infty ) )

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

suppose left_improper_integral (f,a,b) = +infty ; :: thesis: ( f is_left_improper_integrable_on a,c & ( left_improper_integral (f,a,b) = ext_left_integral (f,a,b) implies left_improper_integral (f,a,c) = (left_improper_integral (f,a,b)) + (integral (f,b,c)) ) & ( left_improper_integral (f,a,b) = +infty implies left_improper_integral (f,a,c) = +infty ) & ( left_improper_integral (f,a,b) = -infty implies left_improper_integral (f,a,c) = -infty ) )

hence ( f is_left_improper_integrable_on a,c & ( left_improper_integral (f,a,b) = ext_left_integral (f,a,b) implies left_improper_integral (f,a,c) = (left_improper_integral (f,a,b)) + (integral (f,b,c)) ) & ( left_improper_integral (f,a,b) = +infty implies left_improper_integral (f,a,c) = +infty ) & ( left_improper_integral (f,a,b) = -infty implies left_improper_integral (f,a,c) = -infty ) ) by A1, A2, A3, A4, A5, Lm13; :: thesis: verum

end;

suppose left_improper_integral (f,a,b) = -infty ; :: thesis: ( f is_left_improper_integrable_on a,c & ( left_improper_integral (f,a,b) = ext_left_integral (f,a,b) implies left_improper_integral (f,a,c) = (left_improper_integral (f,a,b)) + (integral (f,b,c)) ) & ( left_improper_integral (f,a,b) = +infty implies left_improper_integral (f,a,c) = +infty ) & ( left_improper_integral (f,a,b) = -infty implies left_improper_integral (f,a,c) = -infty ) )

hence ( f is_left_improper_integrable_on a,c & ( left_improper_integral (f,a,b) = ext_left_integral (f,a,b) implies left_improper_integral (f,a,c) = (left_improper_integral (f,a,b)) + (integral (f,b,c)) ) & ( left_improper_integral (f,a,b) = +infty implies left_improper_integral (f,a,c) = +infty ) & ( left_improper_integral (f,a,b) = -infty implies left_improper_integral (f,a,c) = -infty ) ) by A1, A2, A3, A4, A5, Lm14; :: thesis: verum

end;

end;

end;

end;