let x0 be Real; :: thesis: for f being PartFunc of REAL,REAL st ex N being Neighbourhood of x0 st N c= dom f & ( for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) holds
( f is_differentiable_in x0 & ( for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) )
let f be PartFunc of REAL,REAL; :: thesis: ( ex N being Neighbourhood of x0 st N c= dom f & ( for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) implies ( f is_differentiable_in x0 & ( for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) ) )
deffunc H₁( Real) -> Element of NAT = 0 ;
defpred S₁[ set ] means $1 in REAL ;
given N being Neighbourhood of x0 such that A1: N c= dom f ; :: thesis: ( ex h being convergent_to_0 Real_Sequence ex c being V8() Real_Sequence st
( rng c = {x0} & rng (h + c) c= dom f & not (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) or ( f is_differentiable_in x0 & ( for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) ) )
assume A2: for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ; :: thesis: ( f is_differentiable_in x0 & ( for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) )
then A3: for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & {x0} c= dom f holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ;
consider r being real number such that
A4: 0 < r and
A5: N = ].(x0 - r),(x0 + r).[ by RCOMP_1:def 6;
consider h being convergent_to_0 Real_Sequence, c being V8() Real_Sequence such that
A6: rng c = {x0} and
A7: rng (h + c) c= dom f and
A8: {x0} c= dom f by A1, Th8;
set l = lim ((h ") (#) ((f /* (h + c)) - (f /* c)));
deffunc H₂( Real) -> Element of REAL = (lim ((h ") (#) ((f /* (h + c)) - (f /* c)))) * $1;
consider L being PartFunc of REAL,REAL such that
A9: for g being Real holds
( g in dom L iff S₁[g] ) and
A10: for g being Real st g in dom L holds
L . g = H₂(g) from SEQ_1:sch 3();
A11: dom L = REAL by A9, FDIFF_1:1;
then A12: for g being Real holds L . g = (lim ((h ") (#) ((f /* (h + c)) - (f /* c)))) * g by A10;
A13: L is total by A11, PARTFUN1:def 2;
deffunc H₃( Real) -> Element of REAL = $1 + x0;
consider T being PartFunc of REAL,REAL such that
A14: for g being Real holds
( g in dom T iff S₁[g] ) and
A15: for g being Real st g in dom T holds
T . g = H₃(g) from SEQ_1:sch 3();
A16: dom T = REAL by A14, FDIFF_1:1;
deffunc H₄( real number ) -> Element of REAL = ((f * T) . $1) - (f . x0);
consider T1 being PartFunc of REAL,REAL such that
A17: for g being Real holds
( g in dom T1 iff S₁[g] ) and
A18: for g being Real st g in dom T1 holds
T1 . g = H₄(g) from SEQ_1:sch 3();
deffunc H₅( Real) -> Element of REAL = (T1 - L) . $1;
A19: dom T1 = REAL by A17, FDIFF_1:1;
then A20: T1 is total by PARTFUN1:def 2;
reconsider L = L as LINEAR by A13, A12, FDIFF_1:def 3;
defpred S₂[ set ] means $1 in ].(- r),r.[;
consider R being PartFunc of REAL,REAL such that
A21: R is total and
A22: for g being Real st g in dom R holds
( ( S₂[g] implies R . g = H₅(g) ) & ( not S₂[g] implies R . g = H₁(g) ) ) from SCHEME1:sch 8();
A23: dom R = REAL by A21, PARTFUN1:def 2;

A24: now

let n be Element of NAT ; :: thesis: c . n = x0
c . n in {x0} by A6, VALUED_0:28;
hence c . n = x0 by TARSKI:def 1; :: thesis: verum

end;

now

let h1 be convergent_to_0 Real_Sequence; :: thesis: ( (h1 ") (#) (R /* h1) is convergent & lim ((h1 ") (#) (R /* h1)) = 0 )
A25: lim h1 = 0 by FDIFF_1:def 1;
h1 is convergent by FDIFF_1:def 1;
then consider k being Element of NAT such that
A26: for n being Element of NAT st k <= n holds
abs ((h1 . n) - 0) < r by A4, A25, SEQ_2:def 7;
set h2 = h1 ^\ k;

A27: now

let n be Element of NAT ; :: thesis: (h1 ^\ k) . n in ].(- r),r.[
abs ((h1 . (n + k)) - 0) < r by A26, NAT_1:12;
then h1 . (n + k) in ].(0 - r),(0 + r).[ by RCOMP_1:1;
hence (h1 ^\ k) . n in ].(- r),r.[ by NAT_1:def 3; :: thesis: verum

end;

A28: rng ((h1 ^\ k) + c) c= dom f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng ((h1 ^\ k) + c) or x in dom f )
assume x in rng ((h1 ^\ k) + c) ; :: thesis: x in dom f
then consider n being Element of NAT such that
A29: x = ((h1 ^\ k) + c) . n by FUNCT_2:113;
(h1 ^\ k) . n in ].(- r),r.[ by A27;
then (h1 ^\ k) . n in { g where g is Real : ( - r < g & g < r ) } by RCOMP_1:def 2;
then A30: ex g being Real st
( g = (h1 ^\ k) . n & - r < g & g < r ) ;
then A31: ((h1 ^\ k) . n) + x0 < x0 + r by XREAL_1:6;
x0 + (- r) < ((h1 ^\ k) . n) + x0 by A30, XREAL_1:6;
then A32: ((h1 ^\ k) . n) + x0 in { g where g is Real : ( x0 - r < g & g < x0 + r ) } by A31;
x = ((h1 ^\ k) . n) + (c . n) by A29, SEQ_1:7
.= ((h1 ^\ k) . n) + x0 by A24 ;
then x in ].(x0 - r),(x0 + r).[ by A32, RCOMP_1:def 2;
hence x in dom f by A1, A5; :: thesis: verum

end;

set b = ((h1 ^\ k) ") (#) (L /* (h1 ^\ k));
set a = ((h1 ^\ k) ") (#) (T1 /* (h1 ^\ k));
A33: ((h1 ") (#) (R /* h1)) ^\ k = ((h1 ") ^\ k) (#) ((R /* h1) ^\ k) by SEQM_3:19
.= ((h1 ^\ k) ") (#) ((R /* h1) ^\ k) by SEQM_3:18
.= ((h1 ^\ k) ") (#) (R /* (h1 ^\ k)) by A21, VALUED_0:29 ;
A34: (((h1 ^\ k) ") (#) (T1 /* (h1 ^\ k))) - (((h1 ^\ k) ") (#) (L /* (h1 ^\ k))) = ((h1 ^\ k) ") (#) ((T1 /* (h1 ^\ k)) - (L /* (h1 ^\ k))) by SEQ_1:21
.= ((h1 ^\ k) ") (#) ((T1 - L) /* (h1 ^\ k)) by A13, A20, RFUNCT_2:13 ;

A35: now

let n be Element of NAT ; :: thesis: ((((h1 ^\ k) ") (#) (T1 /* (h1 ^\ k))) - (((h1 ^\ k) ") (#) (L /* (h1 ^\ k)))) . n = (((h1 ^\ k) ") (#) (R /* (h1 ^\ k))) . n
A36: (h1 ^\ k) . n in ].(- r),r.[ by A27;
thus ((((h1 ^\ k) ") (#) (T1 /* (h1 ^\ k))) - (((h1 ^\ k) ") (#) (L /* (h1 ^\ k)))) . n = (((h1 ^\ k) ") . n) * (((T1 - L) /* (h1 ^\ k)) . n) by A34, SEQ_1:8
.= (((h1 ^\ k) ") . n) * ((T1 - L) . ((h1 ^\ k) . n)) by A13, A20, FUNCT_2:115
.= (((h1 ^\ k) ") . n) * (R . ((h1 ^\ k) . n)) by A22, A23, A36
.= (((h1 ^\ k) ") . n) * ((R /* (h1 ^\ k)) . n) by A21, FUNCT_2:115
.= (((h1 ^\ k) ") (#) (R /* (h1 ^\ k))) . n by SEQ_1:8 ; :: thesis: verum

end;

A37: h1 ^\ k is non-empty by FDIFF_1:def 1;

A38: now

let n be Nat; :: thesis: (((h1 ^\ k) ") (#) (L /* (h1 ^\ k))) . n = lim ((h ") (#) ((f /* (h + c)) - (f /* c)))
A39: n in NAT by ORDINAL1:def 12;
then A40: (h1 ^\ k) . n <> 0 by A37, SEQ_1:5;
thus (((h1 ^\ k) ") (#) (L /* (h1 ^\ k))) . n = (((h1 ^\ k) ") . n) * ((L /* (h1 ^\ k)) . n) by A39, SEQ_1:8
.= (((h1 ^\ k) ") . n) * (L . ((h1 ^\ k) . n)) by A13, A39, FUNCT_2:115
.= (((h1 ^\ k) ") . n) * (((h1 ^\ k) . n) * (lim ((h ") (#) ((f /* (h + c)) - (f /* c))))) by A10, A11
.= ((((h1 ^\ k) ") . n) * ((h1 ^\ k) . n)) * (lim ((h ") (#) ((f /* (h + c)) - (f /* c))))
.= ((((h1 ^\ k) . n) ") * ((h1 ^\ k) . n)) * (lim ((h ") (#) ((f /* (h + c)) - (f /* c)))) by VALUED_1:10
.= 1 * (lim ((h ") (#) ((f /* (h + c)) - (f /* c)))) by A40, XCMPLX_0:def 7
.= lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ; :: thesis: verum

end;

then A41: ((h1 ^\ k) ") (#) (L /* (h1 ^\ k)) is constant by VALUED_0:def 18;

now

let n be Element of NAT ; :: thesis: (((h1 ^\ k) ") (#) (T1 /* (h1 ^\ k))) . n = (((h1 ^\ k) ") (#) ((f /* ((h1 ^\ k) + c)) - (f /* c))) . n
A42: c . n = x0 by A24;
thus (((h1 ^\ k) ") (#) (T1 /* (h1 ^\ k))) . n = (((h1 ^\ k) ") . n) * ((T1 /* (h1 ^\ k)) . n) by SEQ_1:8
.= (((h1 ^\ k) ") . n) * (T1 . ((h1 ^\ k) . n)) by A20, FUNCT_2:115
.= (((h1 ^\ k) ") . n) * (((f * T) . ((h1 ^\ k) . n)) - (f . x0)) by A18, A19
.= (((h1 ^\ k) ") . n) * ((f . (T . ((h1 ^\ k) . n))) - (f . x0)) by A16, FUNCT_1:13
.= (((h1 ^\ k) ") . n) * ((f . (((h1 ^\ k) . n) + x0)) - (f . x0)) by A15, A16
.= (((h1 ^\ k) ") . n) * ((f . (((h1 ^\ k) + c) . n)) - (f . (c . n))) by A42, SEQ_1:7
.= (((h1 ^\ k) ") . n) * ((f . (((h1 ^\ k) + c) . n)) - ((f /* c) . n)) by A6, A8, FUNCT_2:108
.= (((h1 ^\ k) ") . n) * (((f /* ((h1 ^\ k) + c)) . n) - ((f /* c) . n)) by A28, FUNCT_2:108
.= (((h1 ^\ k) ") . n) * (((f /* ((h1 ^\ k) + c)) - (f /* c)) . n) by RFUNCT_2:1
.= (((h1 ^\ k) ") (#) ((f /* ((h1 ^\ k) + c)) - (f /* c))) . n by SEQ_1:8 ; :: thesis: verum

end;

then A43: ((h1 ^\ k) ") (#) (T1 /* (h1 ^\ k)) = ((h1 ^\ k) ") (#) ((f /* ((h1 ^\ k) + c)) - (f /* c)) by FUNCT_2:63;
then A44: ((h1 ^\ k) ") (#) (T1 /* (h1 ^\ k)) is convergent by A2, A6, A28;
then (((h1 ^\ k) ") (#) (T1 /* (h1 ^\ k))) - (((h1 ^\ k) ") (#) (L /* (h1 ^\ k))) is convergent by A41, SEQ_2:11;
then A45: ((h1 ^\ k) ") (#) (R /* (h1 ^\ k)) is convergent by A35, FUNCT_2:63;
hence (h1 ") (#) (R /* h1) is convergent by A33, SEQ_4:21; :: thesis: lim ((h1 ") (#) (R /* h1)) = 0
A46: lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = lim (((h1 ^\ k) ") (#) (T1 /* (h1 ^\ k))) by A3, A6, A7, A8, A28, A43, Th7;
lim (((h1 ^\ k) ") (#) (L /* (h1 ^\ k))) = (((h1 ^\ k) ") (#) (L /* (h1 ^\ k))) . 0 by A41, SEQ_4:25
.= lim ((h ") (#) ((f /* (h + c)) - (f /* c))) by A38 ;
then lim ((((h1 ^\ k) ") (#) (T1 /* (h1 ^\ k))) - (((h1 ^\ k) ") (#) (L /* (h1 ^\ k)))) = (lim ((h ") (#) ((f /* (h + c)) - (f /* c)))) - (lim ((h ") (#) ((f /* (h + c)) - (f /* c)))) by A44, A46, A41, SEQ_2:12
.= 0 ;
then lim (((h1 ^\ k) ") (#) (R /* (h1 ^\ k))) = 0 by A35, FUNCT_2:63;
hence lim ((h1 ") (#) (R /* h1)) = 0 by A45, A33, SEQ_4:22; :: thesis: verum

end;

then reconsider R = R as REST by A21, FDIFF_1:def 2;

A47: now

take N = N; :: thesis: ( N c= dom f & ex L being LINEAR ex R being REST st
( L . 1 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) & ( for g1 being Real st g1 in N holds
(L . (g1 - x0)) + (R . (g1 - x0)) = (f . g1) - (f . x0) ) ) )
thus N c= dom f by A1; :: thesis: ex L being LINEAR ex R being REST st
( L . 1 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) & ( for g1 being Real st g1 in N holds
(L . (g1 - x0)) + (R . (g1 - x0)) = (f . g1) - (f . x0) ) )
take L = L; :: thesis: ex R being REST st
( L . 1 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) & ( for g1 being Real st g1 in N holds
(L . (g1 - x0)) + (R . (g1 - x0)) = (f . g1) - (f . x0) ) )
take R = R; :: thesis: ( L . 1 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) & ( for g1 being Real st g1 in N holds
(L . (g1 - x0)) + (R . (g1 - x0)) = (f . g1) - (f . x0) ) )
thus L . 1 = (lim ((h ") (#) ((f /* (h + c)) - (f /* c)))) * 1 by A10, A11
.= lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ; :: thesis: for g1 being Real st g1 in N holds
(L . (g1 - x0)) + (R . (g1 - x0)) = (f . g1) - (f . x0)
let g1 be Real; :: thesis: ( g1 in N implies (L . (g1 - x0)) + (R . (g1 - x0)) = (f . g1) - (f . x0) )
assume g1 in N ; :: thesis: (L . (g1 - x0)) + (R . (g1 - x0)) = (f . g1) - (f . x0)
then g1 - x0 in ].(- r),r.[ by A5, FCONT_3:2;
hence (L . (g1 - x0)) + (R . (g1 - x0)) = (L . (g1 - x0)) + ((T1 - L) . (g1 - x0)) by A22, A23
.= (L . (g1 - x0)) + ((T1 . (g1 - x0)) - (L . (g1 - x0))) by A13, A20, RFUNCT_1:56
.= ((f * T) . (g1 - x0)) - (f . x0) by A18, A19
.= (f . (T . (g1 - x0))) - (f . x0) by A16, FUNCT_1:13
.= (f . ((g1 - x0) + x0)) - (f . x0) by A15, A16
.= (f . g1) - (f . x0) ;
:: thesis: verum

end;

thus f is_differentiable_in x0 :: thesis: for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c)))

proof

consider N1 being Neighbourhood of x0 such that
A48: N1 c= dom f and
A49: ex L being LINEAR ex R being REST st
( L . 1 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) & ( for g being Real st g in N1 holds
(f . g) - (f . x0) = (L . (g - x0)) + (R . (g - x0)) ) ) by A47;
take N1 ; :: according to FDIFF_1:def 4 :: thesis: ( N1 c= dom f & ex b₁ being Element of K21(K22(REAL,REAL)) ex b₂ being Element of K21(K22(REAL,REAL)) st
for b₃ being Element of REAL holds
( not b₃ in N1 or (f . b₃) - (f . x0) = (b₁ . (b₃ - x0)) + (b₂ . (b₃ - x0)) ) )
thus N1 c= dom f by A48; :: thesis: ex b₁ being Element of K21(K22(REAL,REAL)) ex b₂ being Element of K21(K22(REAL,REAL)) st
for b₃ being Element of REAL holds
( not b₃ in N1 or (f . b₃) - (f . x0) = (b₁ . (b₃ - x0)) + (b₂ . (b₃ - x0)) )
consider L1 being LINEAR, R1 being REST such that
L1 . 1 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) and
A50: for g being Real st g in N1 holds
(f . g) - (f . x0) = (L1 . (g - x0)) + (R1 . (g - x0)) by A49;
take L1 ; :: thesis: ex b₁ being Element of K21(K22(REAL,REAL)) st
for b₂ being Element of REAL holds
( not b₂ in N1 or (f . b₂) - (f . x0) = (L1 . (b₂ - x0)) + (b₁ . (b₂ - x0)) )
take R1 ; :: thesis: for b₁ being Element of REAL holds
( not b₁ in N1 or (f . b₁) - (f . x0) = (L1 . (b₁ - x0)) + (R1 . (b₁ - x0)) )
thus for b₁ being Element of REAL holds
( not b₁ in N1 or (f . b₁) - (f . x0) = (L1 . (b₁ - x0)) + (R1 . (b₁ - x0)) ) by A50; :: thesis: verum

end;

then A51: diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) by A47, FDIFF_1:def 5;
let h1 be convergent_to_0 Real_Sequence; :: thesis: for c being V8() Real_Sequence st rng c = {x0} & rng (h1 + c) c= dom f holds
diff (f,x0) = lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c)))
let c1 be V8() Real_Sequence; :: thesis: ( rng c1 = {x0} & rng (h1 + c1) c= dom f implies diff (f,x0) = lim ((h1 ") (#) ((f /* (h1 + c1)) - (f /* c1))) )
assume that
A52: rng c1 = {x0} and
A53: rng (h1 + c1) c= dom f ; :: thesis: diff (f,x0) = lim ((h1 ") (#) ((f /* (h1 + c1)) - (f /* c1)))
c1 = c by A6, A52, Th5;
hence diff (f,x0) = lim ((h1 ") (#) ((f /* (h1 + c1)) - (f /* c1))) by A3, A6, A7, A8, A51, A53, Th7; :: thesis: verum