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
[#] 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;
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 by FUNCT_1:33;
A5: rng (f ") = dom f by FUNCT_1:33;
A6: for y0 being Element of REAL st y0 in dom (f ") holds
( f " is_differentiable_in y0 & diff ((f "),y0) = 1 / (diff (f,((f ") . y0))) )

proof

let y0 be Element of REAL ; :: thesis: ( y0 in dom (f ") implies ( f " is_differentiable_in y0 & diff ((f "),y0) = 1 / (diff (f,((f ") . y0))) ) )
assume A7: y0 in dom (f ") ; :: thesis: ( f " is_differentiable_in y0 & diff ((f "),y0) = 1 / (diff (f,((f ") . y0))) )
then consider x0 being Element of REAL such that
A8: x0 in dom f and
A9: y0 = f . x0 by A4, PARTFUN1:3;
A10: for h being non-zero 0 -convergent Real_Sequence
for c being constant 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

reconsider fy = (f ") . y0 as Element of REAL by XREAL_0:def 1;
set a = seq_const ((f ") . y0);
let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant 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 constant 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 that
A11: rng c = {y0} and
A12: 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))) )
A13: lim (h + c) = y0 by A11, Th4;
reconsider a = seq_const ((f ") . y0) as constant Real_Sequence ;
defpred S₁[ Element of NAT , Real] means for r1, r2 being Real st r1 = (h + c) . $1 & r2 = a . $1 holds
r1 = f . (r2 + $2);
A14: for n being Element of NAT ex r being Element of REAL st S₁[n,r]

proof

let n be Element of NAT ; :: thesis: ex r being Element of REAL st S₁[n,r]
(h + c) . n in rng (h + c) by VALUED_0:28;
then consider g being Element of REAL such that
g in dom f and
A15: (h + c) . n = f . g by A4, A12, PARTFUN1:3;
take r = g - x0; :: thesis: S₁[n,r]
let r1, r2 be Real; :: thesis: ( r1 = (h + c) . n & r2 = a . n implies r1 = f . (r2 + r) )
assume that
A16: r1 = (h + c) . n and
A17: r2 = a . n ; :: thesis: r1 = f . (r2 + r)
a . n = (f ") . (f . x0) by A9, SEQ_1:57
.= x0 by A8, FUNCT_1:34 ;
hence r1 = f . (r2 + r) by A15, A16, A17; :: thesis: verum

end;

consider b being Real_Sequence such that
A18: for n being Element of NAT holds S₁[n,b . n] from FUNCT_2:sch 3(A14);

A19: now :: thesis: for n being Element of NAT holds c . n = f . x0

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 A9, A11, TARSKI:def 1; :: thesis: verum

end;

now :: thesis: for n being Nat holds not b . n = 0

given n being Nat such that A20: b . n = 0 ; :: thesis: contradiction
A21: n in NAT by ORDINAL1:def 12;
A22: (h + c) . n = (h . n) + (c . n) by SEQ_1:7
.= (h . n) + (f . x0) by A19, A21 ;
f . ((a . n) + (b . n)) = f . ((f ") . (f . x0)) by A9, A20, SEQ_1:57
.= f . x0 by A8, FUNCT_1:34 ;
then (h . n) + (f . x0) = f . x0 by A18, A22, A21;
hence contradiction by SEQ_1:5; :: thesis: verum

end;

then A23: b is non-zero by SEQ_1:5;
A24: [#] REAL c= dom f by A1;
then dom f = REAL ;
then A25: f is total by PARTFUN1:def 2;
A26: y0 in dom ((f ") | (rng f)) by A4, A7, RELAT_1:69;
( f | ([#] REAL) is increasing or f | ([#] REAL) is decreasing ) by A1, A2, Th37, Th38;
then (f ") | (rng f) is continuous by A25, FCONT_3:22;
then (f ") | (dom (f ")) is_continuous_in y0 by A4, A26, FCONT_1:def 2;
then A27: f " is_continuous_in y0 by RELAT_1:68;

A28: now :: thesis: for n being Element of NAT holds (((f ") /* (h + c)) - a) . n = b . n

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:1
.= ((f ") . ((h + c) . n)) - (a . n) by A12, FUNCT_2:108
.= ((f ") . (f . ((b . n) + (a . n)))) - (a . n) by A18
.= ((b . n) + (a . n)) - (a . n) by A24, A29, FUNCT_1:34
.= b . n ; :: thesis: verum

end;

A30: (f ") /* (h + c) is convergent by A12, A13, A27, FCONT_1:def 1;
then ((f ") /* (h + c)) - a is convergent ;
then A31: b is convergent by A28, FUNCT_2:63;
A32: lim a = a . 0 by SEQ_4:26
.= (f ") . y0 by SEQ_1:57 ;
(f ") . y0 = lim ((f ") /* (h + c)) by A12, A13, A27, FCONT_1:def 1;
then lim (((f ") /* (h + c)) - a) = ((f ") . y0) - ((f ") . y0) by A30, A32, SEQ_2:12
.= 0 ;
then A33: lim b = 0 by A28, FUNCT_2:63;
A34: rng (b + a) c= dom f by A24;
reconsider b = b as non-zero 0 -convergent Real_Sequence by A23, A31, A33, FDIFF_1:def 1;
A35: b " is non-zero by SEQ_1:33;
A36: 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 object ; :: 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:113;
then x = (f ") . y0 by SEQ_1:57;
hence x in {((f ") . y0)} by TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: 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 SEQ_1:57;
hence x in rng a by VALUED_0:28; :: thesis: verum

end;

A37: rng a c= dom f

proof

let x be object ; :: 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 A36, TARSKI:def 1;
hence x in dom f by A5, A7, FUNCT_1:def 3; :: thesis: verum

end;

now :: thesis: for n being Element of NAT holds (f /* a) . n = c . n

let n be Element of NAT ; :: thesis: (f /* a) . n = c . n
c . n in rng c by VALUED_0:28;
then A38: c . n = y0 by A11, TARSKI:def 1;
thus (f /* a) . n = f . (a . n) by A37, FUNCT_2:108
.= f . ((f ") . y0) by SEQ_1:57
.= c . n by A4, A7, A38, FUNCT_1:35 ; :: thesis: verum

end;

then A39: f /* a = c ;

now :: thesis: for n being Element of NAT holds h . n = ((f /* (b + a)) - (f /* a)) . n

let n be Element of NAT ; :: thesis: h . n = ((f /* (b + a)) - (f /* a)) . n
(h + c) . n = f . ((a . n) + (b . n)) by A18;
then (h . n) + (c . n) = f . ((a . n) + (b . n)) by SEQ_1:7;
hence h . n = (f . ((b . n) + (a . n))) - ((f /* a) . n) by A39
.= (f . ((b + a) . n)) - ((f /* a) . n) by SEQ_1:7
.= ((f /* (b + a)) . n) - ((f /* a) . n) by A34, FUNCT_2:108
.= ((f /* (b + a)) - (f /* a)) . n by RFUNCT_2:1 ;
:: thesis: verum

end;

then A40: h = (f /* (b + a)) - (f /* a) ;
then (f /* (b + a)) - (f /* a) is non-zero ;
then A41: (b ") (#) ((f /* (b + a)) - (f /* a)) is non-zero by A35, SEQ_1:35;
A42: rng c c= dom (f ") by A7, A11, TARSKI:def 1;

now :: thesis: for n being Element of NAT holds ((h ") (#) (((f ") /* (h + c)) - ((f ") /* c))) . n = (((b ") (#) ((f /* (b + a)) - (f /* a))) ") . n

let n be Element of NAT ; :: thesis: ((h ") (#) (((f ") /* (h + c)) - ((f ") /* c))) . n = (((b ") (#) ((f /* (b + a)) - (f /* a))) ") . n
A43: (a . n) + (b . n) in [#] REAL ;
c . n in rng c by VALUED_0:28;
then A44: c . n = y0 by A11, TARSKI:def 1;
thus ((h ") (#) (((f ") /* (h + c)) - ((f ") /* c))) . n = ((h ") . n) * ((((f ") /* (h + c)) - ((f ") /* c)) . n) by SEQ_1:8
.= ((h ") . n) * ((((f ") /* (h + c)) . n) - (((f ") /* c) . n)) by RFUNCT_2:1
.= ((h ") . n) * (((f ") . ((h + c) . n)) - (((f ") /* c) . n)) by A12, FUNCT_2:108
.= ((h ") . n) * (((f ") . (f . ((a . n) + (b . n)))) - (((f ") /* c) . n)) by A18
.= ((h ") . n) * (((a . n) + (b . n)) - (((f ") /* c) . n)) by A24, A43, FUNCT_1:34
.= ((h ") . n) * (((a . n) + (b . n)) - ((f ") . (c . n))) by A42, FUNCT_2:108
.= ((h ") . n) * (((a . n) + (b . n)) - (a . n)) by A44, SEQ_1:57
.= ((h ") (#) ((b ") ")) . n by SEQ_1:8
.= (((b ") (#) ((f /* (b + a)) - (f /* a))) ") . n by A40, SEQ_1:36 ; :: thesis: verum

end;

then A45: (h ") (#) (((f ") /* (h + c)) - ((f ") /* c)) = ((b ") (#) ((f /* (b + a)) - (f /* a))) " ;
A46: f is_differentiable_in fy by A1, FDIFF_1:9;
then A47: lim ((b ") (#) ((f /* (b + a)) - (f /* a))) = diff (f,((f ") . y0)) by A36, A34, Th12;
diff (f,((f ") . y0)) = diff (f,((f ") . y0)) ;
then A48: (b ") (#) ((f /* (b + a)) - (f /* a)) is convergent by A36, A34, A46, Th12;
A49: 0 <> diff (f,((f ") . y0)) by A2;
hence (h ") (#) (((f ") /* (h + c)) - ((f ") /* c)) is convergent by A45, A41, A48, A47, SEQ_2:21; :: 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 A45, A41, A48, A47, A49, SEQ_2:22
.= 1 / (diff (f,((f ") . y0))) by XCMPLX_1:215 ; :: thesis: verum

end;

ex N being Neighbourhood of y0 st N c= dom (f ") by A3, A4, A7, RCOMP_1:18;
hence ( f " is_differentiable_in y0 & diff ((f "),y0) = 1 / (diff (f,((f ") . y0))) ) by A10, 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:9; :: 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 A6; :: thesis: verum