theorem Th62: :: MESFUN15:60

for f being PartFunc of REAL,REAL
for a, b being Real st a <= b & [.a,b.] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds
( max+ f is_integrable_on ['a,b'] & max- f is_integrable_on ['a,b'] & 2 * (integral ((max+ f),a,b)) = (integral (f,a,b)) + (integral ((abs f),a,b)) & 2 * (integral ((max- f),a,b)) = (- (integral (f,a,b))) + (integral ((abs f),a,b)) & integral (f,a,b) = (integral ((max+ f),a,b)) - (integral ((max- f),a,b)) )