:: deftheorem Def1 defines IntegralFuncs INTEGRA7:def 1 :
for X being set
for f being PartFunc of REAL,REAL
for b₃ being set holds
( b₃ = IntegralFuncs (f,X) iff for x being set holds
( x in b₃ iff ex F being PartFunc of REAL,REAL st
( x = F & F is_differentiable_on X & F `| X = f | X ) ) );