theorem Th19: :: PDLAX:13

for a, b being Real
for u being PartFunc of REAL,REAL st a < b & u is_differentiable_on ].a,b.[ & dom u = ['a,b'] & u is continuous & ( for t being Real st t in ].a,b.[ holds
(u `| ].a,b.[) . t = 0 ) holds
ex C being Real st
for t being Real st t in ['a,b'] holds
u . t = C