theorem Th47: :: INTEGR24:47

for f being PartFunc of REAL,REAL
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))