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

let y0 be Real; :: thesis:
assume A8: y0 in dom ((f | ].p,g.[) ") ; :: thesis:
then consider x0 being Real such that
A9: x0 in dom (f | ].p,g.[) and
A10: y0 = (f | ].p,g.[) . x0 by A5, PARTFUN1:26;
A11: for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {y0} & rng (h + c) c= dom ((f | ].p,g.[) ") holds
( (h ") (#) ((((f | ].p,g.[) ") /* (h + c)) - (((f | ].p,g.[) ") /* c)) is convergent & lim ((h ") (#) ((((f | ].p,g.[) ") /* (h + c)) - (((f | ].p,g.[) ") /* c))) = 1 / (diff (f,(((f | ].p,g.[) ") . y0))) )

A12: ( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing )

proof

per cases by A3;

suppose for x0 being Real st x0 in ].p,g.[ holds
0 < diff (f,x0) ; :: thesis:

hence ( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing ) by A1, A2, ROLLE:9; :: thesis:

end;

suppose for x0 being Real st x0 in ].p,g.[ holds
diff (f,x0) < 0 ; :: thesis:

hence ( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing ) by A1, A2, ROLLE:10; :: thesis:

end;

].p,g.[ c= dom f by A2, FDIFF_1:def 7;
then ((f | ].p,g.[) ") | (f .: ].p,g.[) is continuous by A12, FCONT_3:25;
then A15: ((f | ].p,g.[) ") | (rng (f | ].p,g.[)) is continuous by RELAT_1:148;
y0 in dom (((f | ].p,g.[) ") | (rng (f | ].p,g.[))) by A5, A8, RELAT_1:98;
then ((f | ].p,g.[) ") | (rng (f | ].p,g.[)) is_continuous_in y0 by A15, FCONT_1:def 2;
then A16: (f | ].p,g.[) " is_continuous_in y0 by A5, RELAT_1:97;
reconsider a = NAT --> (((f | ].p,g.[) ") . y0) as Real_Sequence by FUNCOP_1:57;
let h be convergent_to_0 Real_Sequence; :: thesis:
let c be V8() Real_Sequence; :: thesis:
assume that
A17: rng c = {y0} and
A18: rng (h + c) c= dom ((f | ].p,g.[) ") ; :: thesis:
A19: lim (h + c) = y0 by A17, Th4;
reconsider a = a as V8() Real_Sequence ;
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) & r2 + $2 in dom f & r2 + $2 in dom (f | ].p,g.[) );
A20: for n being Element of NAT ex r being Real st S₁[n,r]

proof

let n be Element of NAT ; :: thesis:
(h + c) . n in rng (h + c) by VALUED_0:28;
then consider g being Real such that
A21: g in dom (f | ].p,g.[) and
A22: (h + c) . n = (f | ].p,g.[) . g by A5, A18, PARTFUN1:26;
take r = g - x0; :: thesis:
let r1, r2 be real number ; :: thesis:
assume that
A23: r1 = (h + c) . n and
A24: r2 = a . n ; :: thesis:
A25: a . n = ((f | ].p,g.[) ") . ((f | ].p,g.[) . x0) by A10, FUNCOP_1:13
.= x0 by A9, FUNCT_1:56 ;
hence r1 = f . (r2 + r) by A21, A22, A23, A24, FUNCT_1:70; :: thesis:
g in (dom f) /\ ].p,g.[ by A21, RELAT_1:90;
hence ( r2 + r in dom f & r2 + r in dom (f | ].p,g.[) ) by A21, A25, A24, XBOOLE_0:def 4; :: thesis:

end;

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

A27: now

let n be Element of NAT ; :: thesis:
A28: (h + c) . n = (h + c) . n ;
then A29: (a . n) + (b . n) in dom (f | ].p,g.[) by A26;
thus ((((f | ].p,g.[) ") /* (h + c)) - a) . n = ((((f | ].p,g.[) ") /* (h + c)) . n) - (a . n) by RFUNCT_2:6
.= (((f | ].p,g.[) ") . ((h + c) . n)) - (a . n) by A18, FUNCT_2:185
.= (((f | ].p,g.[) ") . (f . ((a . n) + (b . n)))) - (a . n) by A26
.= (((f | ].p,g.[) ") . ((f | ].p,g.[) . ((a . n) + (b . n)))) - (a . n) by A26, A28, FUNCT_1:70
.= ((a . n) + (b . n)) - (a . n) by A29, FUNCT_1:56
.= b . n ; :: thesis:

end;

A30: h + c is convergent by A17, Th4;
then A31: ((f | ].p,g.[) ") /* (h + c) is convergent by A18, A19, A16, FCONT_1:def 1;
then (((f | ].p,g.[) ") /* (h + c)) - a is convergent by SEQ_2:25;
then A32: b is convergent by A27, FUNCT_2:113;
A33: lim a = a . 0 by SEQ_4:41
.= ((f | ].p,g.[) ") . y0 by FUNCOP_1:13 ;
((f | ].p,g.[) ") . y0 = lim (((f | ].p,g.[) ") /* (h + c)) by A18, A30, A19, A16, FCONT_1:def 1;
then lim ((((f | ].p,g.[) ") /* (h + c)) - a) = (((f | ].p,g.[) ") . y0) - (((f | ].p,g.[) ") . y0) by A31, A33, SEQ_2:26
.= 0 ;
then A34: lim b = 0 by A27, FUNCT_2:113;
A35: rng (b + a) c= dom f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng (b + a) ; :: thesis:
then consider n being Element of NAT such that
A36: x = (b + a) . n by FUNCT_2:190;
A37: (h + c) . n = (h + c) . n ;
x = (a . n) + (b . n) by A36, SEQ_1:11;
hence x in dom f by A26, A37; :: thesis:

end;

((f | ].p,g.[) ") . y0 in dom (f | ].p,g.[) by A6, A8, FUNCT_1:def 5;
then ((f | ].p,g.[) ") . y0 in (dom f) /\ ].p,g.[ by RELAT_1:90;
then A38: ((f | ].p,g.[) ") . y0 in ].p,g.[ by XBOOLE_0:def 4;
then A39: f is_differentiable_in ((f | ].p,g.[) ") . y0 by A2, FDIFF_1:16;

A40: now

let n be Element of NAT ; :: thesis:
c . n in rng c by VALUED_0:28;
hence c . n = (f | ].p,g.[) . x0 by A10, A17, TARSKI:def 1; :: thesis:

end;

A41: 0 <> diff (f,(((f | ].p,g.[) ") . y0)) by A3, A38;
A42: h is non-empty by FDIFF_1:def 1;

now

given n being Element of NAT such that A43: b . n = 0 ; :: thesis:
a . n = ((f | ].p,g.[) ") . ((f | ].p,g.[) . x0) by A10, FUNCOP_1:13
.= x0 by A9, FUNCT_1:56 ;
then A44: f . ((a . n) + (b . n)) = (f | ].p,g.[) . x0 by A9, A43, FUNCT_1:70;
(h + c) . n = (h . n) + (c . n) by SEQ_1:11
.= (h . n) + ((f | ].p,g.[) . x0) by A40 ;
then (h . n) + ((f | ].p,g.[) . x0) = (f | ].p,g.[) . x0 by A26, A44;
hence contradiction by A42, SEQ_1:7; :: thesis:

end;

then A45: b is non-empty by SEQ_1:7;
then reconsider b = b as convergent_to_0 Real_Sequence by A32, A34, FDIFF_1:def 1;
A46: b " is non-empty by A45, SEQ_1:41;
A47: rng a = {(((f | ].p,g.[) ") . y0)}

proof

thus rng a c= {(((f | ].p,g.[) ") . y0)} :: according to XBOOLE_0:def 10 :: thesis:

proof

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

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in {(((f | ].p,g.[) ") . y0)} ; :: thesis:
then x = ((f | ].p,g.[) ") . y0 by TARSKI:def 1;
then a . 0 = x by FUNCOP_1:13;
hence x in rng a by VALUED_0:28; :: thesis:

end;

A48: rng a c= dom f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng a ; :: thesis:
then x = ((f | ].p,g.[) ") . y0 by A47, TARSKI:def 1;
then x = x0 by A9, A10, FUNCT_1:56;
then x in (dom f) /\ ].p,g.[ by A9, RELAT_1:90;
hence x in dom f by XBOOLE_0:def 4; :: thesis:

end;

now

let n be Element of NAT ; :: thesis:
A49: ((f | ].p,g.[) ") . y0 in rng ((f | ].p,g.[) ") by A8, FUNCT_1:def 5;
c . n in rng c by VALUED_0:28;
then A50: c . n = y0 by A17, TARSKI:def 1;
thus (f /* a) . n = f . (a . n) by A48, FUNCT_2:185
.= f . (((f | ].p,g.[) ") . y0) by FUNCOP_1:13
.= (f | ].p,g.[) . (((f | ].p,g.[) ") . y0) by A6, A49, FUNCT_1:70
.= c . n by A5, A8, A50, FUNCT_1:57 ; :: thesis:

end;

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

now

let n be Element of NAT ; :: thesis:
(h + c) . n = f . ((a . n) + (b . n)) by A26;
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 A51
.= (f . ((b + a) . n)) - ((f /* a) . n) by SEQ_1:11
.= ((f /* (b + a)) . n) - ((f /* a) . n) by A35, FUNCT_2:185
.= ((f /* (b + a)) - (f /* a)) . n by RFUNCT_2:6 ;
:: thesis:

end;

then A52: h = (f /* (b + a)) - (f /* a) by FUNCT_2:113;
then (f /* (b + a)) - (f /* a) is non-empty by FDIFF_1:def 1;
then A53: (b ") (#) ((f /* (b + a)) - (f /* a)) is non-empty by A46, SEQ_1:43;
A54: rng c c= dom ((f | ].p,g.[) ")

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng c ; :: thesis:
hence x in dom ((f | ].p,g.[) ") by A8, A17, TARSKI:def 1; :: thesis:

end;

now

let n be Element of NAT ; :: thesis:
A55: (h + c) . n = (h + c) . n ;
then A56: (a . n) + (b . n) in dom (f | ].p,g.[) by A26;
c . n in rng c by VALUED_0:28;
then A57: c . n = y0 by A17, TARSKI:def 1;
thus ((h ") (#) ((((f | ].p,g.[) ") /* (h + c)) - (((f | ].p,g.[) ") /* c))) . n = ((h ") . n) * (((((f | ].p,g.[) ") /* (h + c)) - (((f | ].p,g.[) ") /* c)) . n) by SEQ_1:12
.= ((h ") . n) * (((((f | ].p,g.[) ") /* (h + c)) . n) - ((((f | ].p,g.[) ") /* c) . n)) by RFUNCT_2:6
.= ((h ") . n) * ((((f | ].p,g.[) ") . ((h + c) . n)) - ((((f | ].p,g.[) ") /* c) . n)) by A18, FUNCT_2:185
.= ((h ") . n) * ((((f | ].p,g.[) ") . (f . ((a . n) + (b . n)))) - ((((f | ].p,g.[) ") /* c) . n)) by A26
.= ((h ") . n) * ((((f | ].p,g.[) ") . ((f | ].p,g.[) . ((a . n) + (b . n)))) - ((((f | ].p,g.[) ") /* c) . n)) by A26, A55, FUNCT_1:70
.= ((h ") . n) * (((a . n) + (b . n)) - ((((f | ].p,g.[) ") /* c) . n)) by A56, FUNCT_1:56
.= ((h ") . n) * (((a . n) + (b . n)) - (((f | ].p,g.[) ") . (c . n))) by A54, FUNCT_2:185
.= ((h ") . n) * (((a . n) + (b . n)) - (a . n)) by A57, FUNCOP_1:13
.= ((h ") (#) ((b ") ")) . n by SEQ_1:12
.= (((b ") (#) ((f /* (b + a)) - (f /* a))) ") . n by A52, SEQ_1:44 ; :: thesis:

end;

then A58: (h ") (#) ((((f | ].p,g.[) ") /* (h + c)) - (((f | ].p,g.[) ") /* c)) = ((b ") (#) ((f /* (b + a)) - (f /* a))) " by FUNCT_2:113;
diff (f,(((f | ].p,g.[) ") . y0)) = diff (f,(((f | ].p,g.[) ") . y0)) ;
then A59: (b ") (#) ((f /* (b + a)) - (f /* a)) is convergent by A47, A35, A39, Th12;
A60: lim ((b ") (#) ((f /* (b + a)) - (f /* a))) = diff (f,(((f | ].p,g.[) ") . y0)) by A47, A35, A39, Th12;
hence (h ") (#) ((((f | ].p,g.[) ") /* (h + c)) - (((f | ].p,g.[) ") /* c)) is convergent by A58, A53, A59, A41, SEQ_2:35; :: thesis:
thus lim ((h ") (#) ((((f | ].p,g.[) ") /* (h + c)) - (((f | ].p,g.[) ") /* c))) = (diff (f,(((f | ].p,g.[) ") . y0))) " by A58, A53, A59, A60, A41, SEQ_2:36
.= 1 / (diff (f,(((f | ].p,g.[) ") . y0))) by XCMPLX_1:217 ; :: thesis:

end;

ex N being Neighbourhood of y0 st N c= dom ((f | ].p,g.[) ") by A4, A5, A8, RCOMP_1:39;
hence ( (f | ].p,g.[) " is_differentiable_in y0 & diff (((f | ].p,g.[) "),y0) = 1 / (diff (f,(((f | ].p,g.[) ") . y0))) ) by A11, Th12; :: thesis:

end;

then for y0 being Real st y0 in dom ((f | ].p,g.[) ") holds
(f | ].p,g.[) " is_differentiable_in y0 ;
hence (f | ].p,g.[) " is_differentiable_on dom ((f | ].p,g.[) ") by A4, A5, FDIFF_1:16; :: thesis:
let x0 be Real; :: thesis:
assume x0 in dom ((f | ].p,g.[) ") ; :: thesis:
hence diff (((f | ].p,g.[) "),x0) = 1 / (diff (f,(((f | ].p,g.[) ") . x0))) by A7; :: thesis: