theorem :: INTEGRA7:17

for a, b being Real
for f, F being PartFunc of REAL,REAL
for x, x0 being Real st f | [.a,b.] is continuous & [.a,b.] c= dom f & x in ].a,b.[ & x0 in ].a,b.[ & F is_integral_of f,].a,b.[ holds
F . x = (integral (f,x0,x)) + (F . x0)