let X be set ; :: thesis: for F, f being PartFunc of REAL,REAL st F is_integral_of f,X holds
X c= dom F
let F, f be PartFunc of REAL,REAL; :: thesis: ( F is_integral_of f,X implies X c= dom F )
assume F is_integral_of f,X ; :: thesis: X c= dom F
then F in IntegralFuncs (f,X) by Def2;
then ex G being PartFunc of REAL,REAL st
( F = G & G is_differentiable_on X & G `| X = f | X ) by Def1;
hence X c= dom F by FDIFF_1:def 6; :: thesis: verum