let x, t be Real; :: thesis: ( 0 < t implies for f1, f2 being PartFunc of REAL ,REAL st [.x,(x + t).] c= dom f1 & [.x,(x + t).] c= dom f2 & f1 | [.x,(x + t).] is continuous & f1 is_differentiable_on ].x,(x + t).[ & f2 | [.x,(x + t).] is continuous & f2 is_differentiable_on ].x,(x + t).[ & ( for x1 being Real st x1 in ].x,(x + t).[ holds
diff f2,x1 <> 0 ) holds
ex s being Real st
( 0 < s & s < 1 & ((f1 . (x + t)) - (f1 . x)) / ((f2 . (x + t)) - (f2 . x)) = (diff f1,(x + (s * t))) / (diff f2,(x + (s * t))) ) )
assume A1: 0 < t ; :: thesis: for f1, f2 being PartFunc of REAL ,REAL st [.x,(x + t).] c= dom f1 & [.x,(x + t).] c= dom f2 & f1 | [.x,(x + t).] is continuous & f1 is_differentiable_on ].x,(x + t).[ & f2 | [.x,(x + t).] is continuous & f2 is_differentiable_on ].x,(x + t).[ & ( for x1 being Real st x1 in ].x,(x + t).[ holds
diff f2,x1 <> 0 ) holds
ex s being Real st
( 0 < s & s < 1 & ((f1 . (x + t)) - (f1 . x)) / ((f2 . (x + t)) - (f2 . x)) = (diff f1,(x + (s * t))) / (diff f2,(x + (s * t))) )
let f1, f2 be PartFunc of REAL ,REAL ; :: thesis: ( [.x,(x + t).] c= dom f1 & [.x,(x + t).] c= dom f2 & f1 | [.x,(x + t).] is continuous & f1 is_differentiable_on ].x,(x + t).[ & f2 | [.x,(x + t).] is continuous & f2 is_differentiable_on ].x,(x + t).[ & ( for x1 being Real st x1 in ].x,(x + t).[ holds
diff f2,x1 <> 0 ) implies ex s being Real st
( 0 < s & s < 1 & ((f1 . (x + t)) - (f1 . x)) / ((f2 . (x + t)) - (f2 . x)) = (diff f1,(x + (s * t))) / (diff f2,(x + (s * t))) ) )
assume that
A0: ( [.x,(x + t).] c= dom f1 & [.x,(x + t).] c= dom f2 ) and
A2: ( f1 | [.x,(x + t).] is continuous & f1 is_differentiable_on ].x,(x + t).[ ) and
A3: ( f2 | [.x,(x + t).] is continuous & f2 is_differentiable_on ].x,(x + t).[ ) and
A4: for x1 being Real st x1 in ].x,(x + t).[ holds
diff f2,x1 <> 0 ; :: thesis: ex s being Real st
( 0 < s & s < 1 & ((f1 . (x + t)) - (f1 . x)) / ((f2 . (x + t)) - (f2 . x)) = (diff f1,(x + (s * t))) / (diff f2,(x + (s * t))) )
consider x0 being Real such that
A6: ( x0 in ].x,(x + t).[ & ((f1 . (x + t)) - (f1 . x)) * (diff f2,x0) = ((f2 . (x + t)) - (f2 . x)) * (diff f1,x0) ) by A2, A3, Th5, A1, A0, XREAL_1:31;
take s = (x0 - x) / t; :: thesis: ( 0 < s & s < 1 & ((f1 . (x + t)) - (f1 . x)) / ((f2 . (x + t)) - (f2 . x)) = (diff f1,(x + (s * t))) / (diff f2,(x + (s * t))) )
x0 in { r where r is Real : ( x < r & r < x + t ) } by A6, RCOMP_1:def 2;
then A7: ex g being Real st
( g = x0 & x < g & g < x + t ) ;
then 0 < x0 - x by XREAL_1:52;
then 0 / t < (x0 - x) / t by A1, XREAL_1:76;
hence 0 < s ; :: thesis: ( s < 1 & ((f1 . (x + t)) - (f1 . x)) / ((f2 . (x + t)) - (f2 . x)) = (diff f1,(x + (s * t))) / (diff f2,(x + (s * t))) )
x0 - x < t by A7, XREAL_1:21;
then (x0 - x) / t < t / t by A1, XREAL_1:76;
hence s < 1 by A1, XCMPLX_1:60; :: thesis: ((f1 . (x + t)) - (f1 . x)) / ((f2 . (x + t)) - (f2 . x)) = (diff f1,(x + (s * t))) / (diff f2,(x + (s * t)))
A8: 0 <> (f2 . (x + t)) - (f2 . x) by A3, A4, A1, Th1, A0, XREAL_1:31;
(diff f2,x0) * (((f1 . (x + t)) - (f1 . x)) / (diff f2,x0)) = (((f2 . (x + t)) - (f2 . x)) * (diff f1,x0)) / (diff f2,x0) by A6, XCMPLX_1:75;
then ((f1 . (x + t)) - (f1 . x)) / ((f2 . (x + t)) - (f2 . x)) = (((f2 . (x + t)) - (f2 . x)) * ((diff f1,x0) / (diff f2,x0))) / ((f2 . (x + t)) - (f2 . x)) by A4, A6, XCMPLX_1:88;
then A9: ((f1 . (x + t)) - (f1 . x)) / ((f2 . (x + t)) - (f2 . x)) = (((diff f1,x0) / (diff f2,x0)) / ((f2 . (x + t)) - (f2 . x))) * ((f2 . (x + t)) - (f2 . x)) ;
(s * t) + x = (x0 - x) + x by A1, XCMPLX_1:88;
hence ((f1 . (x + t)) - (f1 . x)) / ((f2 . (x + t)) - (f2 . x)) = (diff f1,(x + (s * t))) / (diff f2,(x + (s * t))) by A8, A9, XCMPLX_1:88; :: thesis: verum