theorem :: INTEGR26:41

for c being Real
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