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 = In (((((f . g) - (f . p)) / (g - p)) * ($1 - p)),REAL);
consider f1 being PartFunc of REAL,REAL such that
A6: ( ( for x being Element of REAL holds
( x in dom f1 iff S₁[x] ) ) & ( for x being Element of REAL st x in dom f1 holds
f1 . x = H₁(x) ) ) from SEQ_1:sch 3();
A7: for x being Real st x in dom f1 holds
f1 . x = (((f . g) - (f . p)) / (g - p)) * (x - p)

proof

let x be Real; :: thesis: ( x in dom f1 implies f1 . x = (((f . g) - (f . p)) / (g - p)) * (x - p) )
assume A8: x in dom f1 ; :: thesis: f1 . x = (((f . g) - (f . p)) / (g - p)) * (x - p)
reconsider x = x as Real ;
f1 . x = H₁(x) by A6, A8;
hence f1 . x = (((f . g) - (f . p)) / (g - p)) * (x - p) ; :: thesis: verum

end;

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

A19: now :: thesis: for x being Real st x in Z holds
f1 . x = ((((f . g) - (f . p)) / (g - p)) * x) + (- ((((f . g) - (f . p)) / (g - p)) * p))

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 A17, A6;
hence f1 . x = (((f . g) - (f . p)) / (g - p)) * (x - p) by A7
.= ((((f . g) - (f . p)) / (g - p)) * x) + (- ((((f . g) - (f . p)) / (g - p)) * p)) ;
:: thesis: verum

end;

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

now :: thesis: for x being Real st x in [.p,g.] holds
f1 . x = ((((f . g) - (f . p)) / (g - p)) * x) + (- ((((f . g) - (f . p)) / (g - p)) * p))

let x be Real; :: 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 A7
.= ((((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 A21: (f - f1) | [.p,g.] is continuous by A4, A10, FCONT_1:18;
A22: g in [.p,g.] by A12, ZFMISC_1:32;
then A23: g in dom f1 by A6;
Z c= dom f by A3, A17;
then Z c= (dom f) /\ (dom f1) by A18, XBOOLE_1:19;
then A24: Z c= dom (f - f1) by VALUED_1:12;
(f - f1) . g = (f . g) - (f1 . g) by A22, A15, VALUED_1:13
.= (f . g) - ((((f . g) - (f . p)) / (g - p)) * (g - p)) by A7, A23
.= (f . g) - ((f . g) - (f . p)) by A2, XCMPLX_1:87
.= (f - f1) . p by A16 ;
then consider x0 being Real such that
A25: x0 in ].p,g.[ and
A26: diff ((f - f1),x0) = 0 by A1, A5, A20, A11, A21, A24, 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, A20, A24, FDIFF_1:19;
then diff ((f - f1),x0) = ((f - f1) `| Z) . x0 by A25, FDIFF_1:def 7
.= (diff (f,x0)) - (diff (f1,x0)) by A5, A20, A24, A25, FDIFF_1:19
.= (diff (f,x0)) - ((f1 `| Z) . x0) by A20, A25, FDIFF_1:def 7 ;
hence ( x0 in ].p,g.[ & diff (f,x0) = ((f . g) - (f . p)) / (g - p) ) by A18, A19, A25, A26, FDIFF_1:23; :: thesis: verum