let f be PartFunc of REAL,REAL; :: thesis: for a, c being Real st ].a,c.[ c= dom f & f is_improper_integrable_on a,c holds
for b1, b2 being Real st a < b1 & b1 < c & a < b2 & b2 < c holds
(left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) = (left_improper_integral (f,a,b2)) + (right_improper_integral (f,b2,c))
let a, c be Real; :: thesis: ( ].a,c.[ c= dom f & f is_improper_integrable_on a,c implies for b1, b2 being Real st a < b1 & b1 < c & a < b2 & b2 < c holds
(left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) = (left_improper_integral (f,a,b2)) + (right_improper_integral (f,b2,c)) )
assume that
A1: ].a,c.[ c= dom f and
A2: f is_improper_integrable_on a,c ; :: thesis: for b1, b2 being Real st a < b1 & b1 < c & a < b2 & b2 < c holds
(left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) = (left_improper_integral (f,a,b2)) + (right_improper_integral (f,b2,c))
let b1, b2 be Real; :: thesis: ( a < b1 & b1 < c & a < b2 & b2 < c implies (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) = (left_improper_integral (f,a,b2)) + (right_improper_integral (f,b2,c)) )
assume that
A3: ( a < b1 & b1 < c ) and
A4: ( a < b2 & b2 < c ) ; :: thesis: (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) = (left_improper_integral (f,a,b2)) + (right_improper_integral (f,b2,c))
consider b being Real such that
A5: ( a < b & b < c ) and
A6: f is_left_improper_integrable_on a,b and
A7: f is_right_improper_integrable_on b,c and
A8: ( not left_improper_integral (f,a,b) = -infty or not right_improper_integral (f,b,c) = +infty ) and
A9: ( not left_improper_integral (f,a,b) = +infty or not right_improper_integral (f,b,c) = -infty ) by A2;

per cases ( ( b1 < b & b2 < b ) or ( b1 < b & b <= b2 ) or ( b <= b1 & b2 < b ) or ( b <= b1 & b <= b2 ) ) ;

suppose ( b1 < b & b2 < b ) ; :: thesis: (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) = (left_improper_integral (f,a,b2)) + (right_improper_integral (f,b2,c))

then ( (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) & (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b2)) + (right_improper_integral (f,b2,c)) ) by A1, A3, A4, A5, A6, A7, A8, A9, Th45;
hence (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) = (left_improper_integral (f,a,b2)) + (right_improper_integral (f,b2,c)) ; :: thesis: verum

end;

suppose ( b1 < b & b <= b2 ) ; :: thesis: (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) = (left_improper_integral (f,a,b2)) + (right_improper_integral (f,b2,c))

then ( (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) & (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b2)) + (right_improper_integral (f,b2,c)) ) by A1, A3, A4, A5, A6, A7, A8, A9, Th45, Th46;
hence (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) = (left_improper_integral (f,a,b2)) + (right_improper_integral (f,b2,c)) ; :: thesis: verum

end;

suppose ( b <= b1 & b2 < b ) ; :: thesis: (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) = (left_improper_integral (f,a,b2)) + (right_improper_integral (f,b2,c))

then ( (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) & (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b2)) + (right_improper_integral (f,b2,c)) ) by A1, A3, A4, A5, A6, A7, A8, A9, Th45, Th46;
hence (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) = (left_improper_integral (f,a,b2)) + (right_improper_integral (f,b2,c)) ; :: thesis: verum

end;

suppose ( b <= b1 & b <= b2 ) ; :: thesis: (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) = (left_improper_integral (f,a,b2)) + (right_improper_integral (f,b2,c))

then ( (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) & (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b2)) + (right_improper_integral (f,b2,c)) ) by A1, A3, A4, A5, A6, A7, A8, A9, Th46;
hence (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) = (left_improper_integral (f,a,b2)) + (right_improper_integral (f,b2,c)) ; :: thesis: verum

end;

end;