let X be set ; :: thesis: for F, f being PartFunc of REAL ,REAL holds
( F is_integral_of f,X iff ( F is_differentiable_on X & F `| X = f | X ) )
let F, f be PartFunc of REAL ,REAL ; :: thesis: ( F is_integral_of f,X iff ( F is_differentiable_on X & F `| X = f | X ) )

hereby :: thesis: ( F is_differentiable_on X & F `| X = f | X implies F is_integral_of f,X )

assume F is_integral_of f,X ; :: thesis: ( F is_differentiable_on X & F `| X = f | X )
then F in IntegralFuncs f,X by Def2;
then ex F9 being PartFunc of REAL ,REAL st
( F = F9 & F9 is_differentiable_on X & F9 `| X = f | X ) by Def1;
hence ( F is_differentiable_on X & F `| X = f | X ) ; :: thesis: verum

end;

assume ( F is_differentiable_on X & F `| X = f | X ) ; :: thesis: F is_integral_of f,X
then F in IntegralFuncs f,X by Def1;
hence F is_integral_of f,X by Def2; :: thesis: verum