theorem Th1: :: ROLLE:1

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