let X be set ; :: thesis: for F, f being PartFunc of , holds
( F is_integral_of f,X iff ( F is_differentiable_on X & F `| X = f | X ) )
let F, f be PartFunc of ,; :: 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 F' being PartFunc of , st
( F = F' & F' is_differentiable_on X & F' `| 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