:: deftheorem Def8 defines integral INTEGR18:def 8 :
for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL, the carrier of X st A c= dom f holds
for b₄ being Element of X holds
( b₄ = integral (f,A) iff ex g being Function of A, the carrier of X st
( g = f | A & b₄ = integral g ) );