let f be PartFunc of REAL,REAL; :: thesis: for I being non empty Interval st I c= dom f & inf I < sup I & f | I = id I holds
( f is_differentiable_on_interval I & ( for x being Real st x in I holds
(f `\ I) . x = 1 ) )
let I be non empty Interval; :: thesis: ( I c= dom f & inf I < sup I & f | I = id I implies ( f is_differentiable_on_interval I & ( for x being Real st x in I holds
(f `\ I) . x = 1 ) ) )
assume that
A1: I c= dom f and
A2: inf I < sup I and
A3: f | I = id I ; :: thesis: ( f is_differentiable_on_interval I & ( for x being Real st x in I holds
(f `\ I) . x = 1 ) )
A4: for x being set st x in I holds
f . x = x

proof

let x be set ; :: thesis: ( x in I implies f . x = x )
assume A5: x in I ; :: thesis: f . x = x
then (f | I) . x = f . x by FUNCT_1:49;
hence f . x = x by A3, A5, FUNCT_1:17; :: thesis: verum

end;

A6: now :: thesis: ( inf I in I implies ( f is_right_differentiable_in lower_bound I & Rdiff (f,(lower_bound I)) = 1 ) )

assume A7: inf I in I ; :: thesis: ( f is_right_differentiable_in lower_bound I & Rdiff (f,(lower_bound I)) = 1 )
then A8: inf I = lower_bound I by Lm5;
consider e being Real such that
A9: ( e > 0 & [.(lower_bound I),((lower_bound I) + e).] c= I ) by A7, A2, Lm14;
A10: ( e > 0 & [.(lower_bound I),((lower_bound I) + e).] c= dom f ) by A1, A9;
A11: for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {(lower_bound I)} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds
( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 1 )

proof

let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant Real_Sequence st rng c = {(lower_bound I)} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds
( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 1 )
let c be constant Real_Sequence; :: thesis: ( rng c = {(lower_bound I)} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) implies ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 1 ) )
assume that
A12: rng c = {(lower_bound I)} and
A13: rng (h + c) c= dom f and
A14: for n being Nat holds h . n > 0 ; :: thesis: ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 1 )
A15: for p being Real st 0 < p holds
ex N being Nat st
for k being Nat st N <= k holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 1).| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex N being Nat st
for k being Nat st N <= k holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 1).| < p )
assume A16: 0 < p ; :: thesis: ex N being Nat st
for k being Nat st N <= k holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 1).| < p
( h is convergent & lim h = 0 ) ;
then consider N being Nat such that
A17: for m being Nat st N <= m holds
|.((h . m) - 0).| < e by A9, SEQ_2:def 7;
take N ; :: thesis: for k being Nat st N <= k holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 1).| < p

hereby :: thesis: verum

let k be Nat; :: thesis: ( N <= k implies |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 1).| < p )
assume A18: N <= k ; :: thesis: |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 1).| < p
(h . k) - 0 > 0 by A14;
then |.((h . k) - 0).| = (h . k) - 0 by COMPLEX1:43;
then A19: ( 0 < h . k & h . k < e ) by A17, A14, A18;
A20: rng c c= I by A7, A8, A12, ZFMISC_1:31;
A21: f /* c = f * c by A1, A7, A8, A12, ZFMISC_1:31, FUNCT_2:def 11;
A22: f /* (h + c) = f * (h + c) by A13, FUNCT_2:def 11;
A23: ( dom (h + c) = NAT & dom c = NAT ) by FUNCT_2:def 1;
then ( k in dom (h + c) & k in dom c ) by ORDINAL1:def 12;
then ( k in dom (f * (h + c)) & k in dom (f * c) ) by A13, A1, A7, A8, A12, ZFMISC_1:31, RELAT_1:27;
then k in (dom (f * (h + c))) /\ (dom (f * c)) by XBOOLE_0:def 4;
then A24: k in dom ((f * (h + c)) - (f * c)) by VALUED_1:12;
A25: dom h = NAT by FUNCT_2:def 1;
then A26: (h + c) - c = h by A23, Th6;
A27: h . k in rng h by A25, ORDINAL1:def 12, FUNCT_1:3;
A28: ( (h + c) . k in rng (h + c) & c . k in rng c ) by A23, ORDINAL1:def 12, FUNCT_1:3;
A29: (h + c) . k = (h . k) + (c . k) by A23, ORDINAL1:def 12, VALUED_1:def 1;
c . k = lower_bound I by A28, A12, TARSKI:def 1;
then ( lower_bound I < (h + c) . k & (h + c) . k < (lower_bound I) + e ) by A19, A29, XREAL_1:8, XREAL_1:29;
then (h + c) . k in [.(lower_bound I),((lower_bound I) + e).] by XXREAL_1:1;
then A30: ( f . ((h + c) . k) = (h + c) . k & f . (c . k) = c . k ) by A4, A28, A9, A20;
((h ") (#) ((f /* (h + c)) - (f /* c))) . k = ((h ") . k) * (((f * (h + c)) - (f * c)) . k) by A21, A22, VALUED_1:5
.= ((h ") . k) * (((f * (h + c)) . k) - ((f * c) . k)) by A24, VALUED_1:13
.= ((h ") . k) * ((f . ((h + c) . k)) - ((f * c) . k)) by A23, ORDINAL1:def 12, FUNCT_1:13
.= ((h ") . k) * (((h + c) . k) - (c . k)) by A30, A23, ORDINAL1:def 12, FUNCT_1:13
.= ((h ") . k) * (h . k) by A25, A26, ORDINAL1:def 12, VALUED_1:13
.= ((h . k) ") * (h . k) by VALUED_1:10
.= 1 by A27, XCMPLX_0:def 7 ;
hence |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 1).| < p by A16, COMPLEX1:44; :: thesis: verum

end;

end;

hence (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by SEQ_2:def 6; :: thesis: lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 1
hence lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 1 by A15, SEQ_2:def 7; :: thesis: verum

end;

then for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {(lower_bound I)} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ;
hence A31: f is_right_differentiable_in lower_bound I by A10, FDIFF_3:def 3; :: thesis: Rdiff (f,(lower_bound I)) = 1
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {(lower_bound I)} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds
lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 1 by A11;
hence Rdiff (f,(lower_bound I)) = 1 by A31, FDIFF_3:def 6; :: thesis: verum

end;

A32: now :: thesis: ( sup I in I implies ( f is_left_differentiable_in upper_bound I & Ldiff (f,(upper_bound I)) = 1 ) )

assume A33: sup I in I ; :: thesis: ( f is_left_differentiable_in upper_bound I & Ldiff (f,(upper_bound I)) = 1 )
then A34: sup I = upper_bound I by Lm6;
consider e being Real such that
A35: ( e > 0 & [.((upper_bound I) - e),(upper_bound I).] c= I ) by A33, A2, Lm15;
A36: ( e > 0 & [.((upper_bound I) - e),(upper_bound I).] c= dom f ) by A1, A35;
A37: for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {(upper_bound I)} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds
( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 1 )

proof

let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant Real_Sequence st rng c = {(upper_bound I)} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds
( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 1 )
let c be constant Real_Sequence; :: thesis: ( rng c = {(upper_bound I)} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) implies ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 1 ) )
assume that
A38: rng c = {(upper_bound I)} and
A39: rng (h + c) c= dom f and
A40: for n being Nat holds h . n < 0 ; :: thesis: ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 1 )
A41: for p being Real st 0 < p holds
ex N being Nat st
for k being Nat st N <= k holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 1).| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex N being Nat st
for k being Nat st N <= k holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 1).| < p )
assume A42: 0 < p ; :: thesis: ex N being Nat st
for k being Nat st N <= k holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 1).| < p
( h is convergent & lim h = 0 ) ;
then consider N being Nat such that
A43: for m being Nat st N <= m holds
|.((h . m) - 0).| < e by A35, SEQ_2:def 7;
take N ; :: thesis: for k being Nat st N <= k holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 1).| < p

hereby :: thesis: verum

let k be Nat; :: thesis: ( N <= k implies |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 1).| < p )
assume A44: N <= k ; :: thesis: |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 1).| < p
(h . k) - 0 < 0 by A40;
then |.((h . k) - 0).| = - ((h . k) - 0) by ABSVALUE:30;
then - (h . k) < e by A44, A43;
then A45: ( - e < h . k & h . k < 0 ) by A40, XREAL_1:25;
A46: rng c c= I by A33, A34, A38, ZFMISC_1:31;
A47: f /* c = f * c by A1, A33, A34, A38, ZFMISC_1:31, FUNCT_2:def 11;
A48: f /* (h + c) = f * (h + c) by A39, FUNCT_2:def 11;
A49: ( dom (h + c) = NAT & dom c = NAT ) by FUNCT_2:def 1;
then ( k in dom (h + c) & k in dom c ) by ORDINAL1:def 12;
then ( k in dom (f * (h + c)) & k in dom (f * c) ) by A39, A1, A33, A34, A38, ZFMISC_1:31, RELAT_1:27;
then k in (dom (f * (h + c))) /\ (dom (f * c)) by XBOOLE_0:def 4;
then A50: k in dom ((f * (h + c)) - (f * c)) by VALUED_1:12;
A51: dom h = NAT by FUNCT_2:def 1;
then A52: (h + c) - c = h by A49, Th6;
A53: h . k in rng h by A51, ORDINAL1:def 12, FUNCT_1:3;
A54: ( (h + c) . k in rng (h + c) & c . k in rng c ) by A49, ORDINAL1:def 12, FUNCT_1:3;
A55: (h + c) . k = (h . k) + (c . k) by A49, ORDINAL1:def 12, VALUED_1:def 1;
c . k = upper_bound I by A54, A38, TARSKI:def 1;
then ( (upper_bound I) - e < (h + c) . k & (h + c) . k < upper_bound I ) by A45, A55, XREAL_1:8, XREAL_1:30;
then (h + c) . k in [.((upper_bound I) - e),(upper_bound I).] by XXREAL_1:1;
then A56: ( f . ((h + c) . k) = (h + c) . k & f . (c . k) = c . k ) by A4, A54, A35, A46;
((h ") (#) ((f /* (h + c)) - (f /* c))) . k = ((h ") . k) * (((f * (h + c)) - (f * c)) . k) by A47, A48, VALUED_1:5
.= ((h ") . k) * (((f * (h + c)) . k) - ((f * c) . k)) by A50, VALUED_1:13
.= ((h ") . k) * ((f . ((h + c) . k)) - ((f * c) . k)) by A49, ORDINAL1:def 12, FUNCT_1:13
.= ((h ") . k) * (((h + c) . k) - (c . k)) by A56, A49, ORDINAL1:def 12, FUNCT_1:13
.= ((h ") . k) * (h . k) by A51, A52, ORDINAL1:def 12, VALUED_1:13
.= ((h . k) ") * (h . k) by VALUED_1:10
.= 1 by A53, XCMPLX_0:def 7 ;
hence |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 1).| < p by A42, COMPLEX1:44; :: thesis: verum

end;

end;

hence (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by SEQ_2:def 6; :: thesis: lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 1
hence lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 1 by A41, SEQ_2:def 7; :: thesis: verum

end;

then for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {(upper_bound I)} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ;
hence A57: f is_left_differentiable_in upper_bound I by A36, FDIFF_3:def 4; :: thesis: Ldiff (f,(upper_bound I)) = 1
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {(upper_bound I)} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds
lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 1 by A37;
hence Ldiff (f,(upper_bound I)) = 1 by A57, FDIFF_3:def 5; :: thesis: verum

end;

set J = ].(inf I),(sup I).[;
A58: ].(inf I),(sup I).[ c= I by Lm13;
then A59: ].(inf I),(sup I).[ c= dom f by A1;
then A60: dom (f | ].(inf I),(sup I).[) = ].(inf I),(sup I).[ by RELAT_1:62;
A61: for x being set st x in ].(inf I),(sup I).[ holds
(f | ].(inf I),(sup I).[) . x = x

proof

let x be set ; :: thesis: ( x in ].(inf I),(sup I).[ implies (f | ].(inf I),(sup I).[) . x = x )
assume A62: x in ].(inf I),(sup I).[ ; :: thesis: (f | ].(inf I),(sup I).[) . x = x
(f | ].(inf I),(sup I).[) . x = f . x by A62, FUNCT_1:49;
hence (f | ].(inf I),(sup I).[) . x = x by A4, A62, A58; :: thesis: verum

end;

for x being Real st x in ].(inf I),(sup I).[ holds
f | ].(inf I),(sup I).[ is_differentiable_in x

proof

let x be Real; :: thesis: ( x in ].(inf I),(sup I).[ implies f | ].(inf I),(sup I).[ is_differentiable_in x )
assume A63: x in ].(inf I),(sup I).[ ; :: thesis: f | ].(inf I),(sup I).[ is_differentiable_in x
then ( inf I < x & x < sup I ) by XXREAL_1:4;
then consider Z being open Subset of REAL such that
A64: ( x in Z & Z c= ].(inf I),(sup I).[ ) by Lm9;
consider N being Neighbourhood of x such that
A65: N c= Z by A64, RCOMP_1:18;
A66: N c= dom (f | ].(inf I),(sup I).[) by A60, A64, A65;
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x} & rng (h + c) c= dom (f | ].(inf I),(sup I).[) holds
(h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c)) is convergent

proof

let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant Real_Sequence st rng c = {x} & rng (h + c) c= dom (f | ].(inf I),(sup I).[) holds
(h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c)) is convergent
let c be constant Real_Sequence; :: thesis: ( rng c = {x} & rng (h + c) c= dom (f | ].(inf I),(sup I).[) implies (h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c)) is convergent )
assume that
A67: rng c = {x} and
A68: rng (h + c) c= dom (f | ].(inf I),(sup I).[) ; :: thesis: (h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c)) is convergent
for p being Real st 0 < p holds
ex N being Nat st
for k being Nat st N <= k holds
|.((((h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c))) . k) - 1).| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex N being Nat st
for k being Nat st N <= k holds
|.((((h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c))) . k) - 1).| < p )
assume A69: 0 < p ; :: thesis: ex N being Nat st
for k being Nat st N <= k holds
|.((((h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c))) . k) - 1).| < p
take N = 0 ; :: thesis: for k being Nat st N <= k holds
|.((((h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c))) . k) - 1).| < p
thus for k being Nat st N <= k holds
|.((((h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c))) . k) - 1).| < p :: thesis: verum

proof

let k be Nat; :: thesis: ( N <= k implies |.((((h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c))) . k) - 1).| < p )
assume N <= k ; :: thesis: |.((((h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c))) . k) - 1).| < p
A70: rng c c= dom (f | ].(inf I),(sup I).[) by A60, A63, A67, ZFMISC_1:31;
A71: ( (f | ].(inf I),(sup I).[) /* (h + c) = (f | ].(inf I),(sup I).[) * (h + c) & (f | ].(inf I),(sup I).[) /* c = (f | ].(inf I),(sup I).[) * c ) by A68, A60, A63, A67, ZFMISC_1:31, FUNCT_2:def 11;
A72: ( dom (h + c) = NAT & dom c = NAT ) by FUNCT_2:def 1;
then ( k in dom (h + c) & k in dom c ) by ORDINAL1:def 12;
then ( k in dom ((f | ].(inf I),(sup I).[) * (h + c)) & k in dom ((f | ].(inf I),(sup I).[) * c) ) by A68, A60, A63, A67, ZFMISC_1:31, RELAT_1:27;
then k in (dom ((f | ].(inf I),(sup I).[) * (h + c))) /\ (dom ((f | ].(inf I),(sup I).[) * c)) by XBOOLE_0:def 4;
then A73: k in dom (((f | ].(inf I),(sup I).[) * (h + c)) - ((f | ].(inf I),(sup I).[) * c)) by VALUED_1:12;
( (h + c) . k in rng (h + c) & c . k in rng c ) by A72, ORDINAL1:def 12, FUNCT_1:3;
then A74: ( (f | ].(inf I),(sup I).[) . ((h + c) . k) = (h + c) . k & (f | ].(inf I),(sup I).[) . (c . k) = c . k ) by A60, A61, A70, A68;
A75: dom h = NAT by FUNCT_2:def 1;
then A76: (h + c) - c = h by A72, Th6;
A77: h . k in rng h by A75, ORDINAL1:def 12, FUNCT_1:3;
((h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c))) . k = ((h ") . k) * ((((f | ].(inf I),(sup I).[) * (h + c)) - ((f | ].(inf I),(sup I).[) * c)) . k) by A71, VALUED_1:5
.= ((h ") . k) * ((((f | ].(inf I),(sup I).[) * (h + c)) . k) - (((f | ].(inf I),(sup I).[) * c) . k)) by A73, VALUED_1:13
.= ((h ") . k) * (((f | ].(inf I),(sup I).[) . ((h + c) . k)) - (((f | ].(inf I),(sup I).[) * c) . k)) by A72, ORDINAL1:def 12, FUNCT_1:13
.= ((h ") . k) * (((h + c) . k) - (c . k)) by A74, A72, ORDINAL1:def 12, FUNCT_1:13
.= ((h ") . k) * (h . k) by A75, A76, ORDINAL1:def 12, VALUED_1:13
.= ((h . k) ") * (h . k) by VALUED_1:10
.= 1 by A77, XCMPLX_0:def 7 ;
hence |.((((h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c))) . k) - 1).| < p by A69, COMPLEX1:44; :: thesis: verum

end;

end;

hence (h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c)) is convergent by SEQ_2:def 6; :: thesis: verum

end;

hence f | ].(inf I),(sup I).[ is_differentiable_in x by A66, FDIFF_2:11; :: thesis: verum

end;

then f is_differentiable_on ].(inf I),(sup I).[ by A59;
hence A78: f is_differentiable_on_interval I by A1, A2, A6, A32; :: thesis: for x being Real st x in I holds
(f `\ I) . x = 1
thus for x being Real st x in I holds
(f `\ I) . x = 1 :: thesis: verum

proof

let x be Real; :: thesis: ( x in I implies (f `\ I) . x = 1 )
assume A79: x in I ; :: thesis: (f `\ I) . x = 1

per cases ( x = inf I or x = sup I or ( x <> inf I & x <> sup I ) ) ;

suppose A80: x = inf I ; :: thesis: (f `\ I) . x = 1

then x = lower_bound I by A79, Lm5;
hence (f `\ I) . x = 1 by A6, A78, A79, A80, Def2; :: thesis: verum

end;

suppose A81: x = sup I ; :: thesis: (f `\ I) . x = 1

then x = upper_bound I by A79, Lm6;
hence (f `\ I) . x = 1 by A78, A79, A81, A32, Def2; :: thesis: verum

end;

suppose A82: ( x <> inf I & x <> sup I ) ; :: thesis: (f `\ I) . x = 1

then A83: (f `\ I) . x = diff (f,x) by A78, A79, Def2;
( inf I <= x & x <= sup I ) by A79, XXREAL_2:61, XXREAL_2:62;
then ( inf I < x & x < sup I ) by A82, XXREAL_0:1;
then consider Z being open Subset of REAL such that
A84: ( x in Z & Z c= ].(inf I),(sup I).[ ) by Lm9;
A85: Z c= dom f by A1, A58, A84;
then A86: dom (f | Z) = dom (id Z) by RELAT_1:62;
for p being Element of REAL st p in dom (f | Z) holds
(f | Z) . p = (id Z) . p

proof

let p be Element of REAL ; :: thesis: ( p in dom (f | Z) implies (f | Z) . p = (id Z) . p )
assume A87: p in dom (f | Z) ; :: thesis: (f | Z) . p = (id Z) . p
then A88: ( p in dom f & p in Z ) by RELAT_1:57;
Z c= I by A84, A58;
then (f | I) | Z = f | Z by RELAT_1:74;
then (f | Z) . p = (f | I) . p by A87, FUNCT_1:49
.= p by A3, A88, A84, A58, FUNCT_1:18 ;
hence (f | Z) . p = (id Z) . p by A87, FUNCT_1:18; :: thesis: verum

end;

then A89: f | Z = id Z by A86, PARTFUN1:5;
then A90: ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 1 ) ) by A85, FDIFF_1:17;
(f `| Z) . x = 1 by A84, A89, A85, FDIFF_1:17;
hence (f `\ I) . x = 1 by A83, A84, A90, FDIFF_1:def 7; :: thesis: verum

end;

end;

end;