theorem Th45: :: INTEGR24:45

for f being PartFunc of REAL,REAL
for a, b, c being Real st ].a,c.[ c= dom f & a < b & b < c & f is_left_improper_integrable_on a,b & f is_right_improper_integrable_on b,c & ( not left_improper_integral (f,a,b) = -infty or not right_improper_integral (f,b,c) = +infty ) & ( not left_improper_integral (f,a,b) = +infty or not right_improper_integral (f,b,c) = -infty ) holds
for b1 being Real st a < b1 & b1 <= b holds
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))