theorem Th42: :: INTEGR19:42
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for g being Function of A,(REAL-NS n) st f = g & f is bounded & f is integrable holds
( g is integrable & integral f = integral g )