theorem Th7: :: ROLLE:7

for p, g being Real
for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
diff (f,x) = 0 ) holds
f | ].p,g.[ is constant