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))) ) ) )
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 h being convergent_to_0 Real_Sequence, c being V8() Real_Sequence such that
A4: ( rng c = {x0} & rng (h + c) c= dom f & {x0} c= dom f ) by A1, Th8;
set l = lim ((h " ) (#) ((f /* (h + c)) - (f /* c)));
defpred S₁[ set ] means $1 in REAL ;
deffunc H₁( Real) -> Element of REAL = (lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))) * $1;
consider L being PartFunc of REAL ,REAL such that
A5: for g being Real holds
( g in dom L iff S₁[g] ) and
A6: for g being Real st g in dom L holds
L . g = H₁(g) from SEQ_1:sch 3();
deffunc H₂( Real) -> Element of REAL = $1 + x0;
consider T being PartFunc of REAL ,REAL such that
A7: for g being Real holds
( g in dom T iff S₁[g] ) and
A8: for g being Real st g in dom T holds
T . g = H₂(g) from SEQ_1:sch 3();
deffunc H₃( real number ) -> Element of REAL = ((f * T) . $1) - (f . x0);
consider T1 being PartFunc of REAL ,REAL such that
A9: for g being Real holds
( g in dom T1 iff S₁[g] ) and
A10: for g being Real st g in dom T1 holds
T1 . g = H₃(g) from SEQ_1:sch 3();
consider r being real number such that
A11: ( 0 < r & N = ].(x0 - r),(x0 + r).[ ) by RCOMP_1:def 7;
defpred S₂[ set ] means $1 in ].(- r),r.[;
deffunc H₄( Real) -> Element of REAL = (T1 - L) . $1;
deffunc H₅( Real) -> Element of NAT = 0 ;
consider R being PartFunc of REAL ,REAL such that
A12: R is total and
A13: 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();
A14: dom L = REAL by A5, FDIFF_1:1;
then A15: L is total by PARTFUN1:def 4;
for g being Real holds L . g = (lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))) * g by A6, A14;
then reconsider L = L as LINEAR by A15, FDIFF_1:def 4;
A16: dom T1 = REAL by A9, FDIFF_1:1;
then A17: T1 is total by PARTFUN1:def 4;
A18: dom T = REAL by A7, FDIFF_1:1;
A19: dom R = REAL by A12, PARTFUN1:def 4;

A20: now

let n be Element of NAT ; :: thesis: c . n = x0
c . n in {x0} by A4, 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 )
( h1 is convergent & lim h1 = 0 & h1 is non-zero ) by FDIFF_1:def 1;
then consider k being Element of NAT such that
A21: for n being Element of NAT st k <= n holds
abs ((h1 . n) - 0 ) < r by A11, SEQ_2:def 7;
set h2 = h1 ^\ k;

A22: now

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

end;

A23: ( h1 ^\ k is convergent & lim (h1 ^\ k) = 0 & h1 ^\ k is non-zero ) by FDIFF_1:def 1;
set a = ((h1 ^\ k) " ) (#) (T1 /* (h1 ^\ k));
A24: 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
A25: x = ((h1 ^\ k) + c) . n by FUNCT_2:190;
A26: x = ((h1 ^\ k) . n) + (c . n) by A25, SEQ_1:11
.= ((h1 ^\ k) . n) + x0 by A20 ;
(h1 ^\ k) . n in ].(- r),r.[ by A22;
then (h1 ^\ k) . n in { g where g is Real : ( - r < g & g < r ) } by RCOMP_1:def 2;
then A27: ex g being Real st
( g = (h1 ^\ k) . n & - r < g & g < r ) ;
then A28: x0 + (- r) < ((h1 ^\ k) . n) + x0 by XREAL_1:8;
((h1 ^\ k) . n) + x0 < x0 + r by A27, XREAL_1:8;
then ((h1 ^\ k) . n) + x0 in { g where g is Real : ( x0 - r < g & g < x0 + r ) } by A28;
then x in ].(x0 - r),(x0 + r).[ by A26, RCOMP_1:def 2;
hence x in dom f by A1, A11; :: thesis: verum

end;

now

let n be Element of NAT ; :: thesis: (((h1 ^\ k) " ) (#) (T1 /* (h1 ^\ k))) . n = (((h1 ^\ k) " ) (#) ((f /* ((h1 ^\ k) + c)) - (f /* c))) . n
A29: c . n = x0 by A20;
thus (((h1 ^\ k) " ) (#) (T1 /* (h1 ^\ k))) . n = (((h1 ^\ k) " ) . n) * ((T1 /* (h1 ^\ k)) . n) by SEQ_1:12
.= (((h1 ^\ k) " ) . n) * (T1 . ((h1 ^\ k) . n)) by A17, FUNCT_2:192
.= (((h1 ^\ k) " ) . n) * (((f * T) . ((h1 ^\ k) . n)) - (f . x0)) by A10, A16
.= (((h1 ^\ k) " ) . n) * ((f . (T . ((h1 ^\ k) . n))) - (f . x0)) by A18, FUNCT_1:23
.= (((h1 ^\ k) " ) . n) * ((f . (((h1 ^\ k) . n) + x0)) - (f . x0)) by A8, A18
.= (((h1 ^\ k) " ) . n) * ((f . (((h1 ^\ k) + c) . n)) - (f . (c . n))) by A29, SEQ_1:11
.= (((h1 ^\ k) " ) . n) * ((f . (((h1 ^\ k) + c) . n)) - ((f /* c) . n)) by A4, FUNCT_2:185
.= (((h1 ^\ k) " ) . n) * (((f /* ((h1 ^\ k) + c)) . n) - ((f /* c) . n)) by A24, FUNCT_2:185
.= (((h1 ^\ k) " ) . n) * (((f /* ((h1 ^\ k) + c)) - (f /* c)) . n) by RFUNCT_2:6
.= (((h1 ^\ k) " ) (#) ((f /* ((h1 ^\ k) + c)) - (f /* c))) . n by SEQ_1:12 ; :: thesis: verum

end;

then A30: ((h1 ^\ k) " ) (#) (T1 /* (h1 ^\ k)) = ((h1 ^\ k) " ) (#) ((f /* ((h1 ^\ k) + c)) - (f /* c)) by FUNCT_2:113;
then A31: ((h1 ^\ k) " ) (#) (T1 /* (h1 ^\ k)) is convergent by A2, A4, A24;
A32: lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = lim (((h1 ^\ k) " ) (#) (T1 /* (h1 ^\ k))) by A3, A4, A24, A30, Th7;
set b = ((h1 ^\ k) " ) (#) (L /* (h1 ^\ k));

A33: now

let n be Nat; :: thesis: (((h1 ^\ k) " ) (#) (L /* (h1 ^\ k))) . n = lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))
X: n in NAT by ORDINAL1:def 13;
then A34: (h1 ^\ k) . n <> 0 by A23, SEQ_1:7;
thus (((h1 ^\ k) " ) (#) (L /* (h1 ^\ k))) . n = (((h1 ^\ k) " ) . n) * ((L /* (h1 ^\ k)) . n) by X, SEQ_1:12
.= (((h1 ^\ k) " ) . n) * (L . ((h1 ^\ k) . n)) by A15, X, FUNCT_2:192
.= (((h1 ^\ k) " ) . n) * (((h1 ^\ k) . n) * (lim ((h " ) (#) ((f /* (h + c)) - (f /* c))))) by A6, A14
.= ((((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 A34, XCMPLX_0:def 7
.= lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) ; :: thesis: verum

end;

then A35: ((h1 ^\ k) " ) (#) (L /* (h1 ^\ k)) is constant by VALUED_0:def 18;
then A36: ((h1 ^\ k) " ) (#) (L /* (h1 ^\ k)) is convergent ;
A37: lim (((h1 ^\ k) " ) (#) (L /* (h1 ^\ k))) = (((h1 ^\ k) " ) (#) (L /* (h1 ^\ k))) . 0 by A35, SEQ_4:40
.= lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) by A33 ;
A38: (((h1 ^\ k) " ) (#) (T1 /* (h1 ^\ k))) - (((h1 ^\ k) " ) (#) (L /* (h1 ^\ k))) is convergent by A31, A36, SEQ_2:25;
A39: 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 A31, A32, A36, A37, SEQ_2:26
.= 0 ;
A40: (((h1 ^\ k) " ) (#) (T1 /* (h1 ^\ k))) - (((h1 ^\ k) " ) (#) (L /* (h1 ^\ k))) = ((h1 ^\ k) " ) (#) ((T1 /* (h1 ^\ k)) - (L /* (h1 ^\ k))) by SEQ_1:29
.= ((h1 ^\ k) " ) (#) ((T1 - L) /* (h1 ^\ k)) by A15, A17, RFUNCT_2:32 ;
A41: T1 - L is total by A15, A17;

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
A42: (h1 ^\ k) . n in ].(- r),r.[ by A22;
thus ((((h1 ^\ k) " ) (#) (T1 /* (h1 ^\ k))) - (((h1 ^\ k) " ) (#) (L /* (h1 ^\ k)))) . n = (((h1 ^\ k) " ) . n) * (((T1 - L) /* (h1 ^\ k)) . n) by A40, SEQ_1:12
.= (((h1 ^\ k) " ) . n) * ((T1 - L) . ((h1 ^\ k) . n)) by A41, FUNCT_2:192
.= (((h1 ^\ k) " ) . n) * (R . ((h1 ^\ k) . n)) by A13, A19, A42
.= (((h1 ^\ k) " ) . n) * ((R /* (h1 ^\ k)) . n) by A12, FUNCT_2:192
.= (((h1 ^\ k) " ) (#) (R /* (h1 ^\ k))) . n by SEQ_1:12 ; :: thesis: verum

end;

then A43: ( ((h1 ^\ k) " ) (#) (R /* (h1 ^\ k)) is convergent & lim (((h1 ^\ k) " ) (#) (R /* (h1 ^\ k))) = 0 ) by A38, A39, FUNCT_2:113;
A44: ((h1 " ) (#) (R /* h1)) ^\ k = ((h1 " ) ^\ k) (#) ((R /* h1) ^\ k) by SEQM_3:42
.= ((h1 ^\ k) " ) (#) ((R /* h1) ^\ k) by SEQM_3:41
.= ((h1 ^\ k) " ) (#) (R /* (h1 ^\ k)) by A12, VALUED_0:29 ;
hence (h1 " ) (#) (R /* h1) is convergent by A43, SEQ_4:35; :: thesis: lim ((h1 " ) (#) (R /* h1)) = 0
thus lim ((h1 " ) (#) (R /* h1)) = 0 by A43, A44, SEQ_4:36; :: thesis: verum

end;

then reconsider R = R as REST by A12, FDIFF_1:def 3;

A45: 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 A6, A14
.= 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 A11, FCONT_3:10;
hence (L . (g1 - x0)) + (R . (g1 - x0)) = (L . (g1 - x0)) + ((T1 - L) . (g1 - x0)) by A13, A19
.= (L . (g1 - x0)) + ((T1 . (g1 - x0)) - (L . (g1 - x0))) by A15, A17, RFUNCT_1:72
.= ((f * T) . (g1 - x0)) - (f . x0) by A10, A16
.= (f . (T . (g1 - x0))) - (f . x0) by A18, FUNCT_1:23
.= (f . ((g1 - x0) + x0)) - (f . x0) by A8, A18
.= (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
A46: N1 c= dom f and
A47: 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 A45;
take N1 ; :: according to FDIFF_1:def 5 :: 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 A46; :: 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
A48: ( L1 . 1 = lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) & ( for g being Real st g in N1 holds
(f . g) - (f . x0) = (L1 . (g - x0)) + (R1 . (g - x0)) ) ) by A47;
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 A48; :: thesis: verum

end;

then A49: diff f,x0 = lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) by A45, FDIFF_1:def 6;
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 A50: ( rng c1 = {x0} & rng (h1 + c1) c= dom f ) ; :: thesis: diff f,x0 = lim ((h1 " ) (#) ((f /* (h1 + c1)) - (f /* c1)))
then c1 = c by A4, Th5;
hence diff f,x0 = lim ((h1 " ) (#) ((f /* (h1 + c1)) - (f /* c1))) by A3, A4, A49, A50, Th7; :: thesis: verum