:: deftheorem defines is_integral_of INTEGRA7:def 2 :
for X being set
for F, f being PartFunc of REAL,REAL holds
( F is_integral_of f,X iff F in IntegralFuncs (f,X) );