theorem Th5:
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)) )