theorem Th30: :: INTEGR19:30

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