let x, t be Real; :: thesis: ( 0 < t implies for f being PartFunc of REAL,REAL st [.x,(x + t).] c= dom f & f | [.x,(x + t).] is continuous & f is_differentiable_on ].x,(x + t).[ holds
ex s being Real st
( 0 < s & s < 1 & f . (x + t) = (f . x) + (t * (diff (f,(x + (s * t))))) ) )
assume A1: 0 < t ; :: thesis: for f being PartFunc of REAL,REAL st [.x,(x + t).] c= dom f & f | [.x,(x + t).] is continuous & f is_differentiable_on ].x,(x + t).[ holds
ex s being Real st
( 0 < s & s < 1 & f . (x + t) = (f . x) + (t * (diff (f,(x + (s * t))))) )
let f be PartFunc of REAL,REAL; :: thesis: ( [.x,(x + t).] c= dom f & f | [.x,(x + t).] is continuous & f is_differentiable_on ].x,(x + t).[ implies ex s being Real st
( 0 < s & s < 1 & f . (x + t) = (f . x) + (t * (diff (f,(x + (s * t))))) ) )
assume ( [.x,(x + t).] c= dom f & f | [.x,(x + t).] is continuous & f is_differentiable_on ].x,(x + t).[ ) ; :: thesis: ex s being Real st
( 0 < s & s < 1 & f . (x + t) = (f . x) + (t * (diff (f,(x + (s * t))))) )
then consider x0 being Real such that
A2: x0 in ].x,(x + t).[ and
A3: diff (f,x0) = ((f . (x + t)) - (f . x)) / ((x + t) - x) by A1, Th3, XREAL_1:29;
take s = (x0 - x) / t; :: thesis: ( 0 < s & s < 1 & f . (x + t) = (f . x) + (t * (diff (f,(x + (s * t))))) )
x0 in { r where r is Real : ( x < r & r < x + t ) } by A2, RCOMP_1:def 2;
then A4: ex g being Real st
( g = x0 & x < g & g < x + t ) ;
then 0 < x0 - x by XREAL_1:50;
then 0 / t < (x0 - x) / t by A1, XREAL_1:74;
hence 0 < s ; :: thesis: ( s < 1 & f . (x + t) = (f . x) + (t * (diff (f,(x + (s * t))))) )
x0 - x < t by A4, XREAL_1:19;
then (x0 - x) / t < t / t by A1, XREAL_1:74;
hence s < 1 by A1, XCMPLX_1:60; :: thesis: f . (x + t) = (f . x) + (t * (diff (f,(x + (s * t)))))
A5: (s * t) + x = (x0 - x) + x by A1, XCMPLX_1:87;
(f . x) + (t * (diff (f,x0))) = (f . x) + ((f . (x + t)) - (f . x)) by A1, A3, XCMPLX_1:87;
hence f . (x + t) = (f . x) + (t * (diff (f,(x + (s * t))))) by A5; :: thesis: verum