theorem Th41: :: ORDEQ_01:41

for n being non zero Element of NAT
for a, b being Real
for f being PartFunc of REAL,(REAL-NS n) st ].a,b.[ c= dom f & f is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (f,x) = 0. (REAL-NS n) ) holds
f | ].a,b.[ is constant