let c be Real; :: thesis: for f, F, G being PartFunc of REAL,REAL
for I being non empty Interval st I c= dom f & F is_antiderivative_of f,I & I c= dom G & ( for x being Real st x in I holds
G . x = (F . x) + c ) holds
G is_antiderivative_of f,I
let f, F, G be PartFunc of REAL,REAL; :: thesis: for I being non empty Interval st I c= dom f & F is_antiderivative_of f,I & I c= dom G & ( for x being Real st x in I holds
G . x = (F . x) + c ) holds
G is_antiderivative_of f,I
let I be non empty Interval; :: thesis: ( I c= dom f & F is_antiderivative_of f,I & I c= dom G & ( for x being Real st x in I holds
G . x = (F . x) + c ) implies G is_antiderivative_of f,I )
assume that
A1: I c= dom f and
A2: F is_antiderivative_of f,I and
A3: I c= dom G and
A4: for x being Real st x in I holds
G . x = (F . x) + c ; :: thesis: G is_antiderivative_of f,I
A5: ( I c= dom F & inf I < sup I ) by A2, FDIFF_12:def 1;
reconsider c0 = c as Element of REAL by XREAL_0:def 1;
deffunc H₁( Element of REAL ) -> Element of REAL = c0;
consider F0 being Function of REAL,REAL such that
A6: for x being Element of REAL holds F0 . x = H₁(x) from FUNCT_2:sch 4();
set G0 = F0 | I;
dom F0 = REAL by FUNCT_2:def 1;
then A7: dom (F0 | I) = I by RELAT_1:62;

A8: now :: thesis: for y being object st y in rng (F0 | I) holds
y in {c}

let y be object ; :: thesis: ( y in rng (F0 | I) implies y in {c} )
assume y in rng (F0 | I) ; :: thesis: y in {c}
then consider x being Element of REAL such that
A9: ( x in dom (F0 | I) & (F0 | I) . x = y ) by PARTFUN1:3;
(F0 | I) . x = F0 . x by A9, FUNCT_1:47;
then (F0 | I) . x = c by A6;
hence y in {c} by A9, TARSKI:def 1; :: thesis: verum

end;

then A10: rng (F0 | I) c= {c} ;

now :: thesis: for y being object st y in {c} holds
y in rng (F0 | I)

let y be object ; :: thesis: ( y in {c} implies y in rng (F0 | I) )
assume y in {c} ; :: thesis: y in rng (F0 | I)
then A11: y = c by TARSKI:def 1;
consider x being object such that
A12: x in I by XBOOLE_0:def 1;
reconsider x = x as Element of REAL by A12;
(F0 | I) . x = F0 . x by A12, FUNCT_1:49;
then (F0 | I) . x = c by A6;
hence y in rng (F0 | I) by A7, A12, A11, FUNCT_1:3; :: thesis: verum

end;

then {c} c= rng (F0 | I) ;
then A13: rng (F0 | I) = {c} by A10, XBOOLE_0:def 10;
then A14: ( F0 | I is_differentiable_on_interval I & ( for x being Real st x in I holds
((F0 | I) `\ I) . x = 0 ) ) by A5, A7, FDIFF_12:15;
A15: dom (F | I) = I by A5, RELAT_1:62;
A16: dom ((F | I) + (F0 | I)) = (dom (F | I)) /\ (dom (F0 | I)) by VALUED_1:def 1;
A17: F | I is_differentiable_on_interval I by A2, Th15;
A18: dom (f | I) = I by A1, RELAT_1:62;

now :: thesis: for x being Element of REAL st x in dom (G | I) holds
(G | I) . x = ((F | I) + (F0 | I)) . x

let x be Element of REAL ; :: thesis: ( x in dom (G | I) implies (G | I) . x = ((F | I) + (F0 | I)) . x )
assume A19: x in dom (G | I) ; :: thesis: (G | I) . x = ((F | I) + (F0 | I)) . x
then (G | I) . x = G . x by FUNCT_1:47;
then A20: (G | I) . x = (F . x) + c by A19, A4;
A21: F . x = (F | I) . x by A19, A15, FUNCT_1:47;
(F0 | I) . x in {c} by A7, A19, A8, FUNCT_1:3;
then (F0 | I) . x = c by TARSKI:def 1;
hence (G | I) . x = ((F | I) + (F0 | I)) . x by A16, A15, A7, A19, A20, A21, VALUED_1:def 1; :: thesis: verum

end;

then A22: G | I = (F | I) + (F0 | I) by A16, A15, A7, A3, RELAT_1:62, PARTFUN1:5;
then A23: G | I is_differentiable_on_interval I by A16, A15, A7, A14, A17, FDIFF_12:19;
then A24: G is_differentiable_on_interval I by Th15;
then A25: dom (G `\ I) = I by FDIFF_12:def 2;

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

let x be Element of REAL ; :: thesis: ( x in dom (G `\ I) implies (G `\ I) . x = (f | I) . x )
assume A26: x in dom (G `\ I) ; :: thesis: (G `\ I) . x = (f | I) . x
then A27: ((F0 | I) `\ I) . x = 0 by A13, A25, A5, A7, FDIFF_12:15;
G `\ I = (G | I) `\ I by A24, Th16;
then (G `\ I) . x = (((F | I) `\ I) . x) + (((F0 | I) `\ I) . x) by A22, A25, A26, A16, A15, A7, A17, A14, FDIFF_12:19;
hence (G `\ I) . x = (f | I) . x by A27, A2, Th16; :: thesis: verum

end;

hence G is_antiderivative_of f,I by A23, A18, A25, Th15, PARTFUN1:5; :: thesis: verum