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 non-zero 0 -convergent Real_Sequence
for c being constant 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 non-zero 0 -convergent Real_Sequence
for c being constant 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 non-zero 0 -convergent Real_Sequence
for c being constant 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 non-zero 0 -convergent Real_Sequence
for c being constant 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 REAL = In (0,REAL);
defpred S₁[ object ] means $1 in REAL ;
given N being Neighbourhood of x0 such that A1: N c= dom f ; :: thesis: ( ex h being non-zero 0 -convergent Real_Sequence ex c being constant 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 non-zero 0 -convergent Real_Sequence
for c being constant 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 non-zero 0 -convergent Real_Sequence
for c being constant 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 non-zero 0 -convergent Real_Sequence
for c being constant 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 non-zero 0 -convergent Real_Sequence
for c being constant 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 such that
A4: 0 < r and
A5: N = ].(x0 - r),(x0 + r).[ by RCOMP_1:def 6;
consider h being non-zero 0 -convergent Real_Sequence, c being constant 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 = In (((lim ((h ") (#) ((f /* (h + c)) - (f /* c)))) * $1),REAL);
consider L being PartFunc of REAL,REAL such that
A9: for g being Element of REAL holds
( g in dom L iff S₁[g] ) and
A10: for g being Element of REAL st g in dom L holds
L . g = H₂(g) from SEQ_1:sch 3();
for g being Real holds
( g in dom L iff S₁[g] ) by A9;
then A11: dom L = REAL by FDIFF_1:1;
A12: for g being Real holds L . g = (lim ((h ") (#) ((f /* (h + c)) - (f /* c)))) * g

proof

let g be Real; :: thesis: L . g = (lim ((h ") (#) ((f /* (h + c)) - (f /* c)))) * g
reconsider gg = g as Element of REAL by XREAL_0:def 1;
A13: gg in dom L by A11;
thus L . g = L . gg
.= H₂(gg) by A13, A10
.= (lim ((h ") (#) ((f /* (h + c)) - (f /* c)))) * gg
.= (lim ((h ") (#) ((f /* (h + c)) - (f /* c)))) * g ; :: thesis: verum

end;

A14: L is total by A11, PARTFUN1:def 2;
deffunc H₃( Real) -> Element of REAL = In (($1 + x0),REAL);
consider T being PartFunc of REAL,REAL such that
A15: for g being Element of REAL holds
( g in dom T iff S₁[g] ) and
A16: for g being Element of REAL st g in dom T holds
T . g = H₃(g) from SEQ_1:sch 3();
for g being Real holds
( g in dom T iff S₁[g] ) by A15;
then A17: dom T = REAL by FDIFF_1:1;
deffunc H₄( Real) -> Element of REAL = In ((((f * T) . $1) - (f . x0)),REAL);
consider T1 being PartFunc of REAL,REAL such that
A18: for g being Element of REAL holds
( g in dom T1 iff S₁[g] ) and
A19: for g being Element of REAL st g in dom T1 holds
T1 . g = H₄(g) from SEQ_1:sch 3();
deffunc H₅( Real) -> Element of REAL = In (((T1 - L) . $1),REAL);
for g being Real holds
( g in dom T1 iff S₁[g] ) by A18;
then A20: dom T1 = REAL by FDIFF_1:1;
then A21: T1 is total by PARTFUN1:def 2;
reconsider L = L as LinearFunc by A14, A12, FDIFF_1:def 3;
defpred S₂[ set ] means $1 in ].(- r),r.[;
consider R being PartFunc of REAL,REAL such that
A22: R is total and
A23: for g being Element of 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();
A24: dom R = REAL by A22, PARTFUN1:def 2;

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

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 :: thesis: for h1 being non-zero 0 -convergent Real_Sequence holds
( (h1 ") (#) (R /* h1) is convergent & lim ((h1 ") (#) (R /* h1)) = 0 )

let h1 be non-zero 0 -convergent Real_Sequence; :: thesis: ( (h1 ") (#) (R /* h1) is convergent & lim ((h1 ") (#) (R /* h1)) = 0 )
A26: lim h1 = 0 ;
consider k being Nat such that
A27: for n being Nat st k <= n holds
|.((h1 . n) - 0).| < r by A4, A26, SEQ_2:def 7;
set h2 = h1 ^\ k;

A28: now :: thesis: for n being Element of NAT holds (h1 ^\ k) . n in ].(- r),r.[

let n be Element of NAT ; :: thesis: (h1 ^\ k) . n in ].(- r),r.[
|.((h1 . (n + k)) - 0).| < r by A27, 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;

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

proof

let x be object ; :: 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
A30: x = ((h1 ^\ k) + c) . n by FUNCT_2:113;
(h1 ^\ k) . n in ].(- r),r.[ by A28;
then (h1 ^\ k) . n in { g where g is Real : ( - r < g & g < r ) } by RCOMP_1:def 2;
then A31: ex g being Real st
( g = (h1 ^\ k) . n & - r < g & g < r ) ;
then A32: ((h1 ^\ k) . n) + x0 < x0 + r by XREAL_1:6;
x0 + (- r) < ((h1 ^\ k) . n) + x0 by A31, XREAL_1:6;
then A33: ((h1 ^\ k) . n) + x0 in { g where g is Real : ( x0 - r < g & g < x0 + r ) } by A32;
x = ((h1 ^\ k) . n) + (c . n) by A30, SEQ_1:7
.= ((h1 ^\ k) . n) + x0 by A25 ;
then x in ].(x0 - r),(x0 + r).[ by A33, 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));
A34: ((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 A22, VALUED_0:29 ;
A35: (((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 A14, A21, RFUNCT_2:13 ;

A36: now :: thesis: for n being Element of NAT holds ((((h1 ^\ k) ") (#) (T1 /* (h1 ^\ k))) - (((h1 ^\ k) ") (#) (L /* (h1 ^\ k)))) . n = (((h1 ^\ k) ") (#) (R /* (h1 ^\ k))) . n

let n be Element of NAT ; :: thesis: ((((h1 ^\ k) ") (#) (T1 /* (h1 ^\ k))) - (((h1 ^\ k) ") (#) (L /* (h1 ^\ k)))) . n = (((h1 ^\ k) ") (#) (R /* (h1 ^\ k))) . n
A37: (h1 ^\ k) . n in ].(- r),r.[ by A28;
thus ((((h1 ^\ k) ") (#) (T1 /* (h1 ^\ k))) - (((h1 ^\ k) ") (#) (L /* (h1 ^\ k)))) . n = (((h1 ^\ k) ") . n) * (((T1 - L) /* (h1 ^\ k)) . n) by A35, SEQ_1:8
.= (((h1 ^\ k) ") . n) * ((T1 - L) . ((h1 ^\ k) . n)) by A14, A21, FUNCT_2:115
.= (((h1 ^\ k) ") . n) * H₅((h1 ^\ k) . n)
.= (((h1 ^\ k) ") . n) * (R . ((h1 ^\ k) . n)) by A23, A24, A37
.= (((h1 ^\ k) ") . n) * ((R /* (h1 ^\ k)) . n) by A22, FUNCT_2:115
.= (((h1 ^\ k) ") (#) (R /* (h1 ^\ k))) . n by SEQ_1:8 ; :: thesis: verum

end;

reconsider ll = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) as Element of REAL by XREAL_0:def 1;

A38: now :: thesis: for n being Nat holds (((h1 ^\ k) ") (#) (L /* (h1 ^\ k))) . n = ll

let n be Nat; :: thesis: (((h1 ^\ k) ") (#) (L /* (h1 ^\ k))) . n = ll
A39: n in NAT by ORDINAL1:def 12;
A40: (h1 ^\ k) . n <> 0 by SEQ_1:5;
A41: (h1 ^\ k) . n in dom L by A11, XREAL_0:def 1;
thus (((h1 ^\ k) ") (#) (L /* (h1 ^\ k))) . n = (((h1 ^\ k) ") . n) * ((L /* (h1 ^\ k)) . n) by SEQ_1:8
.= (((h1 ^\ k) ") . n) * (L . ((h1 ^\ k) . n)) by A14, A39, FUNCT_2:115
.= (((h1 ^\ k) ") . n) * H₂((h1 ^\ k) . n) by A10, A41
.= ((((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
.= ll ; :: thesis: verum

end;

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

now :: thesis: for n being Element of NAT holds (((h1 ^\ k) ") (#) (T1 /* (h1 ^\ k))) . n = (((h1 ^\ k) ") (#) ((f /* ((h1 ^\ k) + c)) - (f /* c))) . n

let n be Element of NAT ; :: thesis: (((h1 ^\ k) ") (#) (T1 /* (h1 ^\ k))) . n = (((h1 ^\ k) ") (#) ((f /* ((h1 ^\ k) + c)) - (f /* c))) . n
A43: c . n = x0 by A25;
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 A21, FUNCT_2:115
.= (((h1 ^\ k) ") . n) * H₄((h1 ^\ k) . n) by A19, A20
.= (((h1 ^\ k) ") . n) * (((f * T) . ((h1 ^\ k) . n)) - (f . x0))
.= (((h1 ^\ k) ") . n) * ((f . (T . ((h1 ^\ k) . n))) - (f . x0)) by A17, FUNCT_1:13
.= (((h1 ^\ k) ") . n) * ((f . H₃((h1 ^\ k) . n)) - (f . x0)) by A17, A16
.= (((h1 ^\ k) ") . n) * ((f . (((h1 ^\ k) . n) + x0)) - (f . x0))
.= (((h1 ^\ k) ") . n) * ((f . (((h1 ^\ k) + c) . n)) - (f . (c . n))) by A43, 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 A29, 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 A44: ((h1 ^\ k) ") (#) (T1 /* (h1 ^\ k)) = ((h1 ^\ k) ") (#) ((f /* ((h1 ^\ k) + c)) - (f /* c)) ;
then A45: ((h1 ^\ k) ") (#) (T1 /* (h1 ^\ k)) is convergent by A2, A6, A29;
then (((h1 ^\ k) ") (#) (T1 /* (h1 ^\ k))) - (((h1 ^\ k) ") (#) (L /* (h1 ^\ k))) is convergent by A42;
then A46: ((h1 ^\ k) ") (#) (R /* (h1 ^\ k)) is convergent by A36, FUNCT_2:63;
hence (h1 ") (#) (R /* h1) is convergent by A34, SEQ_4:21; :: thesis: lim ((h1 ") (#) (R /* h1)) = 0
A47: lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = lim (((h1 ^\ k) ") (#) (T1 /* (h1 ^\ k))) by A3, A6, A7, A8, A29, A44, Th7;
lim (((h1 ^\ k) ") (#) (L /* (h1 ^\ k))) = (((h1 ^\ k) ") (#) (L /* (h1 ^\ k))) . 0 by A42, 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 A45, A47, A42, SEQ_2:12
.= 0 ;
then lim (((h1 ^\ k) ") (#) (R /* (h1 ^\ k))) = 0 by A36, FUNCT_2:63;
hence lim ((h1 ") (#) (R /* h1)) = 0 by A46, A34, SEQ_4:22; :: thesis: verum

end;

then reconsider R = R as RestFunc by A22, FDIFF_1:def 2;

A48: now :: thesis: ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc ex R being RestFunc 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 N = N; :: thesis: ( N c= dom f & ex L being LinearFunc ex R being RestFunc 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 LinearFunc ex R being RestFunc 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 RestFunc 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) ) )
1 in REAL by NUMBERS:19;
hence L . 1 = H₂(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 A49: g1 - x0 in ].(- r),r.[ by A5, FCONT_3:2;
reconsider gg1 = g1, xx0 = x0 as Element of REAL by XREAL_0:def 1;
thus (L . (g1 - x0)) + (R . (g1 - x0)) = (L . (g1 - x0)) + H₅(g1 - x0) by A23, A24, A49
.= (L . (g1 - x0)) + ((T1 - L) . (g1 - x0))
.= (L . (gg1 - xx0)) + ((T1 . (g1 - x0)) - (L . (g1 - x0))) by A14, A21, RFUNCT_1:56
.= (L . (gg1 - xx0)) + (H₄(g1 - x0) - (L . (g1 - x0))) by A19, A20
.= ((f * T) . (gg1 - xx0)) - (f . x0)
.= (f . (T . (gg1 - xx0))) - (f . x0) by A17, FUNCT_1:13
.= (f . H₃(gg1 - xx0)) - (f . x0) by A17, A16
.= (f . ((gg1 - xx0) + xx0)) - (f . x0)
.= (f . g1) - (f . x0) ; :: thesis: verum

end;

thus f is_differentiable_in x0 by A48; :: thesis: for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c)))
then A50: diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) by A48, FDIFF_1:def 5;
let h1 be non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant 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 constant 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
A51: rng c1 = {x0} and
A52: rng (h1 + c1) c= dom f ; :: thesis: diff (f,x0) = lim ((h1 ") (#) ((f /* (h1 + c1)) - (f /* c1)))
c1 = c by A6, A51, Th5;
hence diff (f,x0) = lim ((h1 ") (#) ((f /* (h1 + c1)) - (f /* c1))) by A3, A6, A7, A8, A50, A52, Th7; :: thesis: verum