let f be one-to-one PartFunc of REAL ,REAL ; :: thesis: ( [#] REAL c= dom f & f is_differentiable_on [#] REAL & ( for x0 being Real holds 0 < diff f,x0 or for x0 being Real holds diff f,x0 < 0 ) implies ( f is one-to-one & f " is_differentiable_on dom (f " ) & ( for x0 being Real st x0 in dom (f " ) holds
diff (f " ),x0 = 1 / (diff f,((f " ) . x0)) ) ) )
assume that
A0: [#] REAL c= dom f and
A1: f is_differentiable_on [#] REAL and
A2: ( for x0 being Real holds 0 < diff f,x0 or for x0 being Real holds diff f,x0 < 0 ) ; :: thesis: ( f is one-to-one & f " is_differentiable_on dom (f " ) & ( for x0 being Real st x0 in dom (f " ) holds
diff (f " ),x0 = 1 / (diff f,((f " ) . x0)) ) )
A3: rng f is open by A1, A2, Th44, A0;
thus f is one-to-one ; :: thesis: ( f " is_differentiable_on dom (f " ) & ( for x0 being Real st x0 in dom (f " ) holds
diff (f " ),x0 = 1 / (diff f,((f " ) . x0)) ) )
A4: ( dom (f " ) = rng f & rng (f " ) = dom f ) by FUNCT_1:55;
A5: for y0 being Real st y0 in dom (f " ) holds
( f " is_differentiable_in y0 & diff (f " ),y0 = 1 / (diff f,((f " ) . y0)) )

proof

let y0 be Real; :: thesis: ( y0 in dom (f " ) implies ( f " is_differentiable_in y0 & diff (f " ),y0 = 1 / (diff f,((f " ) . y0)) ) )
assume A6: y0 in dom (f " ) ; :: thesis: ( f " is_differentiable_in y0 & diff (f " ),y0 = 1 / (diff f,((f " ) . y0)) )
then consider x0 being Real such that
A7: ( x0 in dom f & y0 = f . x0 ) by A4, PARTFUN1:26;
A8: ex N being Neighbourhood of y0 st N c= dom (f " ) by A3, A4, A6, RCOMP_1:39;
for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {y0} & rng (h + c) c= dom (f " ) holds
( (h " ) (#) (((f " ) /* (h + c)) - ((f " ) /* c)) is convergent & lim ((h " ) (#) (((f " ) /* (h + c)) - ((f " ) /* c))) = 1 / (diff f,((f " ) . y0)) )

proof

let h be convergent_to_0 Real_Sequence; :: thesis: for c being V8() Real_Sequence st rng c = {y0} & rng (h + c) c= dom (f " ) holds
( (h " ) (#) (((f " ) /* (h + c)) - ((f " ) /* c)) is convergent & lim ((h " ) (#) (((f " ) /* (h + c)) - ((f " ) /* c))) = 1 / (diff f,((f " ) . y0)) )
let c be V8() Real_Sequence; :: thesis: ( rng c = {y0} & rng (h + c) c= dom (f " ) implies ( (h " ) (#) (((f " ) /* (h + c)) - ((f " ) /* c)) is convergent & lim ((h " ) (#) (((f " ) /* (h + c)) - ((f " ) /* c))) = 1 / (diff f,((f " ) . y0)) ) )
assume A9: ( rng c = {y0} & rng (h + c) c= dom (f " ) ) ; :: thesis: ( (h " ) (#) (((f " ) /* (h + c)) - ((f " ) /* c)) is convergent & lim ((h " ) (#) (((f " ) /* (h + c)) - ((f " ) /* c))) = 1 / (diff f,((f " ) . y0)) )
reconsider a = NAT --> ((f " ) . y0) as Real_Sequence by FUNCOP_1:57;
reconsider a = a as V8() Real_Sequence ;
A10: rng a = {((f " ) . y0)}

proof

thus rng a c= {((f " ) . y0)} :: according to XBOOLE_0:def 10 :: thesis: {((f " ) . y0)} c= rng a

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng a or x in {((f " ) . y0)} )
assume x in rng a ; :: thesis: x in {((f " ) . y0)}
then ex n being Element of NAT st x = a . n by FUNCT_2:190;
then x = (f " ) . y0 by FUNCOP_1:13;
hence x in {((f " ) . y0)} by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {((f " ) . y0)} or x in rng a )
assume x in {((f " ) . y0)} ; :: thesis: x in rng a
then x = (f " ) . y0 by TARSKI:def 1;
then a . 0 = x by FUNCOP_1:13;
hence x in rng a by VALUED_0:28; :: thesis: verum

end;

A11: now

let n be Element of NAT ; :: thesis: c . n = f . x0
c . n in rng c by VALUED_0:28;
hence c . n = f . x0 by A7, A9, TARSKI:def 1; :: thesis: verum

end;

defpred S₁[ Element of NAT , real number ] means for r1, r2 being real number st r1 = (h + c) . $1 & r2 = a . $1 holds
r1 = f . (r2 + $2);
A12: for n being Element of NAT ex r being Real st S₁[n,r]

proof

let n be Element of NAT ; :: thesis: ex r being Real st S₁[n,r]
(h + c) . n in rng (h + c) by VALUED_0:28;
then consider g being Real such that
A13: ( g in dom f & (h + c) . n = f . g ) by A4, A9, PARTFUN1:26;
A14: a . n = (f " ) . (f . x0) by A7, FUNCOP_1:13
.= x0 by A7, FUNCT_1:56 ;
take r = g - x0; :: thesis: S₁[n,r]
let r1, r2 be real number ; :: thesis: ( r1 = (h + c) . n & r2 = a . n implies r1 = f . (r2 + r) )
assume ( r1 = (h + c) . n & r2 = a . n ) ; :: thesis: r1 = f . (r2 + r)
hence r1 = f . (r2 + r) by A13, A14; :: thesis: verum

end;

consider b being Real_Sequence such that
A15: for n being Element of NAT holds S₁[n,b . n] from FUNCT_2:sch 3(A12);
A16: ( h is non-zero & h is convergent & lim h = 0 ) by FDIFF_1:def 1;

now

given n being Element of NAT such that A17: b . n = 0 ; :: thesis: contradiction
A18: (h + c) . n = (h . n) + (c . n) by SEQ_1:11
.= (h . n) + (f . x0) by A11 ;
f . ((a . n) + (b . n)) = f . ((f " ) . (f . x0)) by A7, A17, FUNCOP_1:13
.= f . x0 by A7, FUNCT_1:56 ;
then (h . n) + (f . x0) = f . x0 by A15, A18;
hence contradiction by A16, SEQ_1:7; :: thesis: verum

end;

then A19: b is non-zero by SEQ_1:7;
A20: ( h + c is convergent & lim (h + c) = y0 ) by A9, Th4;
A21: ( f | ([#] REAL ) is increasing or f | ([#] REAL ) is decreasing ) by A1, A2, Th37, Th38, A0;
X: y0 in dom ((f " ) | (rng f)) by A4, A6, RELAT_1:98;
A22: [#] REAL c= dom f by A1, FDIFF_1:def 7;
then dom f = REAL by XBOOLE_0:def 10;
then f is total by PARTFUN1:def 4;
then (f " ) | (rng f) is continuous by A21, FCONT_3:30;
then (f " ) | (dom (f " )) is_continuous_in y0 by A4, X, FCONT_1:def 2;
then f " is_continuous_in y0 by RELAT_1:97;
then A23: ( (f " ) /* (h + c) is convergent & (f " ) . y0 = lim ((f " ) /* (h + c)) ) by A9, A20, FCONT_1:def 1;
A25: lim a = a . 0 by SEQ_4:41
.= (f " ) . y0 by FUNCOP_1:13 ;
A26: ((f " ) /* (h + c)) - a is convergent by A23, SEQ_2:25;
A27: lim (((f " ) /* (h + c)) - a) = ((f " ) . y0) - ((f " ) . y0) by A23, A25, SEQ_2:26
.= 0 ;
A28: rng (b + a) c= dom f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (b + a) or x in dom f )
assume x in rng (b + a) ; :: thesis: x in dom f
then x in REAL ;
hence x in dom f by A22; :: thesis: verum

end;

now

let n be Element of NAT ; :: thesis: (((f " ) /* (h + c)) - a) . n = b . n
A29: (b . n) + (a . n) in [#] REAL ;
thus (((f " ) /* (h + c)) - a) . n = (((f " ) /* (h + c)) . n) - (a . n) by RFUNCT_2:6
.= ((f " ) . ((h + c) . n)) - (a . n) by A9, FUNCT_2:185
.= ((f " ) . (f . ((b . n) + (a . n)))) - (a . n) by A15
.= ((b . n) + (a . n)) - (a . n) by A22, A29, FUNCT_1:56
.= b . n ; :: thesis: verum

end;

then ( b is convergent & lim b = 0 ) by A26, A27, FUNCT_2:113;
then reconsider b = b as convergent_to_0 Real_Sequence by A19, FDIFF_1:def 1;
A30: rng a c= dom f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng a or x in dom f )
assume x in rng a ; :: thesis: x in dom f
then x = (f " ) . y0 by A10, TARSKI:def 1;
hence x in dom f by A4, A6, FUNCT_1:def 5; :: thesis: verum

end;

now

let n be Element of NAT ; :: thesis: (f /* a) . n = c . n
c . n in rng c by VALUED_0:28;
then A31: c . n = y0 by A9, TARSKI:def 1;
thus (f /* a) . n = f . (a . n) by A30, FUNCT_2:185
.= f . ((f " ) . y0) by FUNCOP_1:13
.= c . n by A4, A6, A31, FUNCT_1:57 ; :: thesis: verum

end;

then A32: f /* a = c by FUNCT_2:113;

now

let n be Element of NAT ; :: thesis: h . n = ((f /* (b + a)) - (f /* a)) . n
(h + c) . n = f . ((a . n) + (b . n)) by A15;
then (h . n) + (c . n) = f . ((a . n) + (b . n)) by SEQ_1:11;
hence h . n = (f . ((b . n) + (a . n))) - ((f /* a) . n) by A32
.= (f . ((b + a) . n)) - ((f /* a) . n) by SEQ_1:11
.= ((f /* (b + a)) . n) - ((f /* a) . n) by A28, FUNCT_2:185
.= ((f /* (b + a)) - (f /* a)) . n by RFUNCT_2:6 ;
:: thesis: verum

end;

then A33: h = (f /* (b + a)) - (f /* a) by FUNCT_2:113;
then A34: (f /* (b + a)) - (f /* a) is non-zero by FDIFF_1:def 1;
A35: rng c c= dom (f " )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng c or x in dom (f " ) )
assume x in rng c ; :: thesis: x in dom (f " )
hence x in dom (f " ) by A6, A9, TARSKI:def 1; :: thesis: verum

end;

A36: b " is non-zero by A19, SEQ_1:41;

now

let n be Element of NAT ; :: thesis: ((h " ) (#) (((f " ) /* (h + c)) - ((f " ) /* c))) . n = (((b " ) (#) ((f /* (b + a)) - (f /* a))) " ) . n
A37: (a . n) + (b . n) in [#] REAL ;
c . n in rng c by VALUED_0:28;
then A38: c . n = y0 by A9, TARSKI:def 1;
thus ((h " ) (#) (((f " ) /* (h + c)) - ((f " ) /* c))) . n = ((h " ) . n) * ((((f " ) /* (h + c)) - ((f " ) /* c)) . n) by SEQ_1:12
.= ((h " ) . n) * ((((f " ) /* (h + c)) . n) - (((f " ) /* c) . n)) by RFUNCT_2:6
.= ((h " ) . n) * (((f " ) . ((h + c) . n)) - (((f " ) /* c) . n)) by A9, FUNCT_2:185
.= ((h " ) . n) * (((f " ) . (f . ((a . n) + (b . n)))) - (((f " ) /* c) . n)) by A15
.= ((h " ) . n) * (((a . n) + (b . n)) - (((f " ) /* c) . n)) by A22, A37, FUNCT_1:56
.= ((h " ) . n) * (((a . n) + (b . n)) - ((f " ) . (c . n))) by A35, FUNCT_2:185
.= ((h " ) . n) * (((a . n) + (b . n)) - (a . n)) by A38, FUNCOP_1:13
.= ((h " ) (#) ((b " ) " )) . n by SEQ_1:12
.= (((b " ) (#) ((f /* (b + a)) - (f /* a))) " ) . n by A33, SEQ_1:44 ; :: thesis: verum

end;

then A39: (h " ) (#) (((f " ) /* (h + c)) - ((f " ) /* c)) = ((b " ) (#) ((f /* (b + a)) - (f /* a))) " by FUNCT_2:113;
A40: (b " ) (#) ((f /* (b + a)) - (f /* a)) is non-zero by A34, A36, SEQ_1:43;
( f is_differentiable_in (f " ) . y0 & diff f,((f " ) . y0) = diff f,((f " ) . y0) ) by A1, FDIFF_1:16;
then A41: ( (b " ) (#) ((f /* (b + a)) - (f /* a)) is convergent & lim ((b " ) (#) ((f /* (b + a)) - (f /* a))) = diff f,((f " ) . y0) ) by A10, A28, Th12;
A42: 0 <> diff f,((f " ) . y0) by A2;
hence (h " ) (#) (((f " ) /* (h + c)) - ((f " ) /* c)) is convergent by A39, A40, A41, SEQ_2:35; :: thesis: lim ((h " ) (#) (((f " ) /* (h + c)) - ((f " ) /* c))) = 1 / (diff f,((f " ) . y0))
thus lim ((h " ) (#) (((f " ) /* (h + c)) - ((f " ) /* c))) = (diff f,((f " ) . y0)) " by A39, A40, A41, A42, SEQ_2:36
.= 1 / (diff f,((f " ) . y0)) by XCMPLX_1:217 ; :: thesis: verum

end;

hence ( f " is_differentiable_in y0 & diff (f " ),y0 = 1 / (diff f,((f " ) . y0)) ) by A8, Th12; :: thesis: verum

end;

then for y0 being Real st y0 in dom (f " ) holds
f " is_differentiable_in y0 ;
hence f " is_differentiable_on dom (f " ) by A3, A4, FDIFF_1:16; :: thesis: for x0 being Real st x0 in dom (f " ) holds
diff (f " ),x0 = 1 / (diff f,((f " ) . x0))
let x0 be Real; :: thesis: ( x0 in dom (f " ) implies diff (f " ),x0 = 1 / (diff f,((f " ) . x0)) )
assume x0 in dom (f " ) ; :: thesis: diff (f " ),x0 = 1 / (diff f,((f " ) . x0))
hence diff (f " ),x0 = 1 / (diff f,((f " ) . x0)) by A5; :: thesis: verum