theorem Th5: :: ROLLE:5

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