theorem :: INTEGR15:19

for n being Element of NAT
for f being PartFunc of REAL,(REAL n)
for A being non empty closed_interval Subset of REAL
for a, b being Real st A = [.a,b.] holds
integral (f,A) = integral (f,a,b)