let f, F be PartFunc of REAL,REAL; :: thesis: for I, J being non empty Interval st inf I < sup I & I c= J & F is_antiderivative_of f,J holds
F is_antiderivative_of f,I
let I, J be non empty Interval; :: thesis: ( inf I < sup I & I c= J & F is_antiderivative_of f,J implies F is_antiderivative_of f,I )
assume that
A1: inf I < sup I and
A2: I c= J and
A3: F is_antiderivative_of f,J ; :: thesis: F is_antiderivative_of f,I
F is_differentiable_on_interval I by A1, A2, A3, FDIFF_12:38;
then A4: dom (F `\ I) = I by FDIFF_12:def 2;
dom (f | J) = J by A3, FDIFF_12:def 2;
then (dom f) /\ J = J by RELAT_1:61;
then A5: dom (f | I) = I by A2, XBOOLE_1:18, RELAT_1:62;

now :: thesis: for x being Element of REAL st x in dom (F `\ I) holds
(F `\ I) . x = (f | I) . x

let x be Element of REAL ; :: thesis: ( x in dom (F `\ I) implies (F `\ I) . x = (f | I) . x )
assume A6: x in dom (F `\ I) ; :: thesis: (F `\ I) . x = (f | I) . x
then (F `\ I) . x = (f | J) . x by A4, A3, A1, A2, FDIFF_12:38;
then (F `\ I) . x = ((f | J) | I) . x by A6, A4, FUNCT_1:49;
hence (F `\ I) . x = (f | I) . x by A2, RELAT_1:74; :: thesis: verum

end;

hence F is_antiderivative_of f,I by A4, A5, A1, A2, A3, FDIFF_12:38, PARTFUN1:5; :: thesis: verum