:: deftheorem Def1 defines is_antiderivative_of INTEGR26:def 1 :
for f, F being PartFunc of REAL,REAL
for I being non empty Interval holds
( F is_antiderivative_of f,I iff ( F is_differentiable_on_interval I & F `\ I = f | I ) );