let p, g be Real; :: thesis: ( p < g implies for f being PartFunc of REAL,REAL st [.p,g.] c= dom f & f | [.p,g.] is continuous & f is_differentiable_on ].p,g.[ holds
ex x0 being Real st
( x0 in ].p,g.[ & diff (f,x0) = ((f . g) - (f . p)) / (g - p) ) )
assume A1: p < g ; :: thesis: for f being PartFunc of REAL,REAL st [.p,g.] c= dom f & f | [.p,g.] is continuous & f is_differentiable_on ].p,g.[ holds
ex x0 being Real st
( x0 in ].p,g.[ & diff (f,x0) = ((f . g) - (f . p)) / (g - p) )
A2: 0 <> g - p by A1;
reconsider Z = ].p,g.[ as open Subset of REAL ;
defpred S₁[ set ] means $1 in [.p,g.];
let f be PartFunc of REAL,REAL; :: thesis: ( [.p,g.] c= dom f & f | [.p,g.] is continuous & f is_differentiable_on ].p,g.[ implies ex x0 being Real st
( x0 in ].p,g.[ & diff (f,x0) = ((f . g) - (f . p)) / (g - p) ) )
assume that
A3: [.p,g.] c= dom f and
A4: f | [.p,g.] is continuous and
A5: f is_differentiable_on ].p,g.[ ; :: thesis: ex x0 being Real st
( x0 in ].p,g.[ & diff (f,x0) = ((f . g) - (f . p)) / (g - p) )
set r = ((f . g) - (f . p)) / (g - p);
deffunc H₁( Real) -> Element of REAL = (((f . g) - (f . p)) / (g - p)) * ($1 - p);
consider f1 being PartFunc of REAL,REAL such that
A6: ( ( for x being Real holds
( x in dom f1 iff S₁[x] ) ) & ( for x being Real st x in dom f1 holds
f1 . x = H₁(x) ) ) from SEQ_1:sch 3();
set f2 = f - f1;
A7: [.p,g.] c= dom f1

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in [.p,g.] or y in dom f1 )
assume y in [.p,g.] ; :: thesis: y in dom f1
hence y in dom f1 by A6; :: thesis: verum

end;

then A8: [.p,g.] c= (dom f) /\ (dom f1) by A3, XBOOLE_1:19;
then A9: [.p,g.] c= dom (f - f1) by VALUED_1:12;
[.p,g.] = ].p,g.[ \/ {p,g} by A1, XXREAL_1:128;
then A10: {p,g} c= [.p,g.] by XBOOLE_1:7;
then A11: p in [.p,g.] by ZFMISC_1:32;
then A12: p in dom f1 by A6;
[.p,g.] c= (dom f) /\ (dom f1) by A3, A7, XBOOLE_1:19;
then A13: [.p,g.] c= dom (f - f1) by VALUED_1:12;
then A14: (f - f1) . p = (f . p) - (f1 . p) by A11, VALUED_1:13
.= (f . p) - ((((f . g) - (f . p)) / (g - p)) * (p - p)) by A6, A12
.= f . p ;
A15: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
then A16: Z c= dom f1 by A7, XBOOLE_1:1;

A17: now

let x be Real; :: thesis: ( x in Z implies f1 . x = ((((f . g) - (f . p)) / (g - p)) * x) + (- ((((f . g) - (f . p)) / (g - p)) * p)) )
assume x in Z ; :: thesis: f1 . x = ((((f . g) - (f . p)) / (g - p)) * x) + (- ((((f . g) - (f . p)) / (g - p)) * p))
then x in dom f1 by A15, A6;
hence f1 . x = (((f . g) - (f . p)) / (g - p)) * (x - p) by A6
.= ((((f . g) - (f . p)) / (g - p)) * x) + (- ((((f . g) - (f . p)) / (g - p)) * p)) ;
:: thesis: verum

end;

then A18: f1 is_differentiable_on Z by A16, FDIFF_1:23;

now

let x be real number ; :: thesis: ( x in [.p,g.] implies f1 . x = ((((f . g) - (f . p)) / (g - p)) * x) + (- ((((f . g) - (f . p)) / (g - p)) * p)) )
assume x in [.p,g.] ; :: thesis: f1 . x = ((((f . g) - (f . p)) / (g - p)) * x) + (- ((((f . g) - (f . p)) / (g - p)) * p))
then x in dom f1 by A6;
hence f1 . x = (((f . g) - (f . p)) / (g - p)) * (x - p) by A6
.= ((((f . g) - (f . p)) / (g - p)) * x) + (- ((((f . g) - (f . p)) / (g - p)) * p)) ;
:: thesis: verum

end;

then f1 | [.p,g.] is continuous by FCONT_1:41;
then A19: (f - f1) | [.p,g.] is continuous by A4, A8, FCONT_1:18;
A20: g in [.p,g.] by A10, ZFMISC_1:32;
then A21: g in dom f1 by A6;
Z c= dom f by A3, A15, XBOOLE_1:1;
then Z c= (dom f) /\ (dom f1) by A16, XBOOLE_1:19;
then A22: Z c= dom (f - f1) by VALUED_1:12;
(f - f1) . g = (f . g) - (f1 . g) by A20, A13, VALUED_1:13
.= (f . g) - ((((f . g) - (f . p)) / (g - p)) * (g - p)) by A6, A21
.= (f . g) - ((f . g) - (f . p)) by A2, XCMPLX_1:87
.= (f - f1) . p by A14 ;
then consider x0 being Real such that
A23: x0 in ].p,g.[ and
A24: diff ((f - f1),x0) = 0 by A1, A5, A18, A9, A19, A22, Th1, FDIFF_1:19;
take x0 ; :: thesis: ( x0 in ].p,g.[ & diff (f,x0) = ((f . g) - (f . p)) / (g - p) )
f - f1 is_differentiable_on Z by A5, A18, A22, FDIFF_1:19;
then diff ((f - f1),x0) = ((f - f1) `| Z) . x0 by A23, FDIFF_1:def 7
.= (diff (f,x0)) - (diff (f1,x0)) by A5, A18, A22, A23, FDIFF_1:19
.= (diff (f,x0)) - ((f1 `| Z) . x0) by A18, A23, FDIFF_1:def 7 ;
hence ( x0 in ].p,g.[ & diff (f,x0) = ((f . g) - (f . p)) / (g - p) ) by A16, A17, A23, A24, FDIFF_1:23; :: thesis: verum