let f, F, G be PartFunc of REAL,REAL; :: thesis: for I being non empty open_interval Subset of REAL st F is_antiderivative_of f,I & G is_antiderivative_of f,I holds
ex c being Real st
for x being Real st x in I holds
F . x = (G . x) + c
let I be non empty open_interval Subset of REAL; :: thesis: ( F is_antiderivative_of f,I & G is_antiderivative_of f,I implies ex c being Real st
for x being Real st x in I holds
F . x = (G . x) + c )
assume that
A1: F is_antiderivative_of f,I and
A2: G is_antiderivative_of f,I ; :: thesis: ex c being Real st
for x being Real st x in I holds
F . x = (G . x) + c
A3: I = ].(inf I),(sup I).[ by MEASURE6:16;
A4: F is_differentiable_on ].(inf I),(sup I).[ by A1, FDIFF_12:def 1;
A5: G is_differentiable_on ].(inf I),(sup I).[ by A2, FDIFF_12:def 1;
A6: ( inf I is R_eal & sup I is R_eal ) by XXREAL_0:def 1;
for x being Real st x in ].(inf I),(sup I).[ holds
diff (F,x) = diff (G,x)

proof

let x be Real; :: thesis: ( x in ].(inf I),(sup I).[ implies diff (F,x) = diff (G,x) )
assume A7: x in ].(inf I),(sup I).[ ; :: thesis: diff (F,x) = diff (G,x)
then ( x <> inf I & x <> sup I ) by XXREAL_1:4;
then ( (F `\ I) . x = diff (F,x) & (G `\ I) . x = diff (G,x) ) by A3, A1, A2, A7, FDIFF_12:def 2;
hence diff (F,x) = diff (G,x) by A1, A2; :: thesis: verum

end;

hence ex c being Real st
for x being Real st x in I holds
F . x = (G . x) + c by A6, A3, A4, A5, Th20; :: thesis: verum