let x, t be Real; ( 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
; 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; ( [.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
A2:
[.x,(x + t).] c= dom f1
and
A3:
[.x,(x + t).] c= dom f2
and
A4:
( f1 | [.x,(x + t).] is continuous & f1 is_differentiable_on ].x,(x + t).[ )
and
A5:
( f2 | [.x,(x + t).] is continuous & f2 is_differentiable_on ].x,(x + t).[ )
and
A6:
for x1 being Real st x1 in ].x,(x + t).[ holds
diff (f2,x1) <> 0
; 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
A7:
x0 in ].x,(x + t).[
and
A8:
((f1 . (x + t)) - (f1 . x)) * (diff (f2,x0)) = ((f2 . (x + t)) - (f2 . x)) * (diff (f1,x0))
by A1, A2, A3, A4, A5, Th5, XREAL_1:29;
(diff (f2,x0)) * (((f1 . (x + t)) - (f1 . x)) / (diff (f2,x0))) = (((f2 . (x + t)) - (f2 . x)) * (diff (f1,x0))) / (diff (f2,x0))
by A8, XCMPLX_1:74;
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 A6, A7, XCMPLX_1:87;
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))
;
take s = (x0 - x) / t; ( 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 A7, RCOMP_1:def 2;
then A10:
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
; ( 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 A10, XREAL_1:19;
then
(x0 - x) / t < t / t
by A1, XREAL_1:74;
hence
s < 1
by A1, XCMPLX_1:60; ((f1 . (x + t)) - (f1 . x)) / ((f2 . (x + t)) - (f2 . x)) = (diff (f1,(x + (s * t)))) / (diff (f2,(x + (s * t))))
A11:
(s * t) + x = (x0 - x) + x
by A1, XCMPLX_1:87;
0 <> (f2 . (x + t)) - (f2 . x)
by A1, A3, A5, A6, Th1, XREAL_1:29;
hence
((f1 . (x + t)) - (f1 . x)) / ((f2 . (x + t)) - (f2 . x)) = (diff (f1,(x + (s * t)))) / (diff (f2,(x + (s * t))))
by A9, A11, XCMPLX_1:87; verum