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