theorem Th47: :: INTEGR19:47

for n being Element of NAT
for a, b being Real
for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f holds
integral (f,b,a) = - (integral (f,a,b))