theorem Th52: :: INTEGR19:52

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