theorem :: INTEGR18:9

for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL, the carrier of X
for g being Function of A, the carrier of X st A c= dom f & f | A = g holds
integral (f,A) = integral g by Def8;