let r, s be Real; :: thesis: ( ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc ex R being RestFunc st

( r = L . 1 & ( for x being Real st x in N holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) & ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc ex R being RestFunc st

( s = L . 1 & ( for x being Real st x in N holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) implies r = s )

assume that

A6: ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc ex R being RestFunc st

( r = L . 1 & ( for x being Real st x in N holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) and

A7: ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc ex R being RestFunc st

( s = L . 1 & ( for x being Real st x in N holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ; :: thesis: r = s

consider N being Neighbourhood of x0 such that

N c= dom f and

A8: ex L being LinearFunc ex R being RestFunc st

( r = L . 1 & ( for x being Real st x in N holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by A6;

consider L being LinearFunc, R being RestFunc such that

A9: r = L . 1 and

A10: for x being Real st x in N holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A8;

consider r1 being Real such that

A11: for p being Real holds L . p = r1 * p by Def3;

consider N1 being Neighbourhood of x0 such that

N1 c= dom f and

A12: ex L being LinearFunc ex R being RestFunc st

( s = L . 1 & ( for x being Real st x in N1 holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by A7;

consider L1 being LinearFunc, R1 being RestFunc such that

A13: s = L1 . 1 and

A14: for x being Real st x in N1 holds

(f . x) - (f . x0) = (L1 . (x - x0)) + (R1 . (x - x0)) by A12;

consider p1 being Real such that

A15: for p being Real holds L1 . p = p1 * p by Def3;

consider N0 being Neighbourhood of x0 such that

A16: ( N0 c= N & N0 c= N1 ) by RCOMP_1:17;

consider g being Real such that

A17: 0 < g and

A18: N0 = ].(x0 - g),(x0 + g).[ by RCOMP_1:def 6;

deffunc H_{1}( Nat) -> set = g / ($1 + 2);

consider s1 being Real_Sequence such that

A19: for n being Nat holds s1 . n = H_{1}(n)
from SEQ_1:sch 1();

( s1 is convergent & lim s1 = 0 ) by A19, SEQ_4:31;

then s1 is 0 -convergent ;

then reconsider h = s1 as non-zero 0 -convergent Real_Sequence by A20;

A21: for n being Element of NAT ex x being Real st

( x in N & x in N1 & h . n = x - x0 )

A24: r = r1 * 1 by A9, A11;

then A36: lim (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) = r - s by SEQ_4:25;

A37: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 ) by Def2;

( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 ) by Def2;

then r - s = 0 - 0 by A36, A37, SEQ_2:12;

hence r = s ; :: thesis: verum

( N c= dom f & ex L being LinearFunc ex R being RestFunc st

( r = L . 1 & ( for x being Real st x in N holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) & ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc ex R being RestFunc st

( s = L . 1 & ( for x being Real st x in N holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) implies r = s )

assume that

A6: ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc ex R being RestFunc st

( r = L . 1 & ( for x being Real st x in N holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) and

A7: ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc ex R being RestFunc st

( s = L . 1 & ( for x being Real st x in N holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ; :: thesis: r = s

consider N being Neighbourhood of x0 such that

N c= dom f and

A8: ex L being LinearFunc ex R being RestFunc st

( r = L . 1 & ( for x being Real st x in N holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by A6;

consider L being LinearFunc, R being RestFunc such that

A9: r = L . 1 and

A10: for x being Real st x in N holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A8;

consider r1 being Real such that

A11: for p being Real holds L . p = r1 * p by Def3;

consider N1 being Neighbourhood of x0 such that

N1 c= dom f and

A12: ex L being LinearFunc ex R being RestFunc st

( s = L . 1 & ( for x being Real st x in N1 holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by A7;

consider L1 being LinearFunc, R1 being RestFunc such that

A13: s = L1 . 1 and

A14: for x being Real st x in N1 holds

(f . x) - (f . x0) = (L1 . (x - x0)) + (R1 . (x - x0)) by A12;

consider p1 being Real such that

A15: for p being Real holds L1 . p = p1 * p by Def3;

consider N0 being Neighbourhood of x0 such that

A16: ( N0 c= N & N0 c= N1 ) by RCOMP_1:17;

consider g being Real such that

A17: 0 < g and

A18: N0 = ].(x0 - g),(x0 + g).[ by RCOMP_1:def 6;

deffunc H

consider s1 being Real_Sequence such that

A19: for n being Nat holds s1 . n = H

now :: thesis: for n being Nat holds 0 <> s1 . n

then A20:
s1 is non-zero
by SEQ_1:5;let n be Nat; :: thesis: 0 <> s1 . n

0 <> g / (n + 2) by A17, XREAL_1:139;

hence 0 <> s1 . n by A19; :: thesis: verum

end;0 <> g / (n + 2) by A17, XREAL_1:139;

hence 0 <> s1 . n by A19; :: thesis: verum

( s1 is convergent & lim s1 = 0 ) by A19, SEQ_4:31;

then s1 is 0 -convergent ;

then reconsider h = s1 as non-zero 0 -convergent Real_Sequence by A20;

A21: for n being Element of NAT ex x being Real st

( x in N & x in N1 & h . n = x - x0 )

proof

A23:
s = p1 * 1
by A13, A15;
let n be Element of NAT ; :: thesis: ex x being Real st

( x in N & x in N1 & h . n = x - x0 )

take x0 + (g / (n + 2)) ; :: thesis: ( x0 + (g / (n + 2)) in N & x0 + (g / (n + 2)) in N1 & h . n = (x0 + (g / (n + 2))) - x0 )

0 + 1 < (n + 1) + 1 by XREAL_1:6;

then g / (n + 2) < g / 1 by A17, XREAL_1:76;

then A22: x0 + (g / (n + 2)) < x0 + g by XREAL_1:6;

0 < g / (n + 2) by A17, XREAL_1:139;

then x0 + (- g) < x0 + (g / (n + 2)) by A17, XREAL_1:6;

then x0 + (g / (n + 2)) in ].(x0 - g),(x0 + g).[ by A22;

hence ( x0 + (g / (n + 2)) in N & x0 + (g / (n + 2)) in N1 & h . n = (x0 + (g / (n + 2))) - x0 ) by A16, A18, A19; :: thesis: verum

end;( x in N & x in N1 & h . n = x - x0 )

take x0 + (g / (n + 2)) ; :: thesis: ( x0 + (g / (n + 2)) in N & x0 + (g / (n + 2)) in N1 & h . n = (x0 + (g / (n + 2))) - x0 )

0 + 1 < (n + 1) + 1 by XREAL_1:6;

then g / (n + 2) < g / 1 by A17, XREAL_1:76;

then A22: x0 + (g / (n + 2)) < x0 + g by XREAL_1:6;

0 < g / (n + 2) by A17, XREAL_1:139;

then x0 + (- g) < x0 + (g / (n + 2)) by A17, XREAL_1:6;

then x0 + (g / (n + 2)) in ].(x0 - g),(x0 + g).[ by A22;

hence ( x0 + (g / (n + 2)) in N & x0 + (g / (n + 2)) in N1 & h . n = (x0 + (g / (n + 2))) - x0 ) by A16, A18, A19; :: thesis: verum

A24: r = r1 * 1 by A9, A11;

A25: now :: thesis: for x being Real st x in N & x in N1 holds

(r * (x - x0)) + (R . (x - x0)) = (s * (x - x0)) + (R1 . (x - x0))

reconsider rs = r - s as Element of REAL by XREAL_0:def 1;(r * (x - x0)) + (R . (x - x0)) = (s * (x - x0)) + (R1 . (x - x0))

let x be Real; :: thesis: ( x in N & x in N1 implies (r * (x - x0)) + (R . (x - x0)) = (s * (x - x0)) + (R1 . (x - x0)) )

assume that

A26: x in N and

A27: x in N1 ; :: thesis: (r * (x - x0)) + (R . (x - x0)) = (s * (x - x0)) + (R1 . (x - x0))

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A10, A26;

then (L . (x - x0)) + (R . (x - x0)) = (L1 . (x - x0)) + (R1 . (x - x0)) by A14, A27;

then (r1 * (x - x0)) + (R . (x - x0)) = (L1 . (x - x0)) + (R1 . (x - x0)) by A11;

hence (r * (x - x0)) + (R . (x - x0)) = (s * (x - x0)) + (R1 . (x - x0)) by A15, A24, A23; :: thesis: verum

end;assume that

A26: x in N and

A27: x in N1 ; :: thesis: (r * (x - x0)) + (R . (x - x0)) = (s * (x - x0)) + (R1 . (x - x0))

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A10, A26;

then (L . (x - x0)) + (R . (x - x0)) = (L1 . (x - x0)) + (R1 . (x - x0)) by A14, A27;

then (r1 * (x - x0)) + (R . (x - x0)) = (L1 . (x - x0)) + (R1 . (x - x0)) by A11;

hence (r * (x - x0)) + (R . (x - x0)) = (s * (x - x0)) + (R1 . (x - x0)) by A15, A24, A23; :: thesis: verum

now :: thesis: for n being Nat holds rs = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n

then
( ((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h)) is V8() & (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . 1 = rs )
by VALUED_0:def 18;
R1 is total
by Def2;

then dom R1 = REAL by PARTFUN1:def 2;

then A28: rng h c= dom R1 ;

let n be Nat; :: thesis: rs = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n

R is total by Def2;

then dom R = REAL by PARTFUN1:def 2;

then A29: rng h c= dom R ;

A30: n in NAT by ORDINAL1:def 12;

then ex x being Real st

( x in N & x in N1 & h . n = x - x0 ) by A21;

then (r * (h . n)) + (R . (h . n)) = (s * (h . n)) + (R1 . (h . n)) by A25;

then A31: ((r * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n)) = ((s * (h . n)) + (R1 . (h . n))) / (h . n) by XCMPLX_1:62;

A32: (R . (h . n)) / (h . n) = (R . (h . n)) * ((h . n) ") by XCMPLX_0:def 9

.= (R . (h . n)) * ((h ") . n) by VALUED_1:10

.= ((R /* h) . n) * ((h ") . n) by A30, A29, FUNCT_2:108

.= ((h ") (#) (R /* h)) . n by SEQ_1:8 ;

A33: h . n <> 0 by SEQ_1:5;

A34: (R1 . (h . n)) / (h . n) = (R1 . (h . n)) * ((h . n) ") by XCMPLX_0:def 9

.= (R1 . (h . n)) * ((h ") . n) by VALUED_1:10

.= ((R1 /* h) . n) * ((h ") . n) by A30, A28, FUNCT_2:108

.= ((h ") (#) (R1 /* h)) . n by SEQ_1:8 ;

A35: (s * (h . n)) / (h . n) = s * ((h . n) / (h . n)) by XCMPLX_1:74

.= s * 1 by A33, XCMPLX_1:60

.= s ;

(r * (h . n)) / (h . n) = r * ((h . n) / (h . n)) by XCMPLX_1:74

.= r * 1 by A33, XCMPLX_1:60

.= r ;

then r + ((R . (h . n)) / (h . n)) = s + ((R1 . (h . n)) / (h . n)) by A31, A35, XCMPLX_1:62;

then r = s + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)) by A32, A34;

hence rs = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n by RFUNCT_2:1; :: thesis: verum

end;then dom R1 = REAL by PARTFUN1:def 2;

then A28: rng h c= dom R1 ;

let n be Nat; :: thesis: rs = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n

R is total by Def2;

then dom R = REAL by PARTFUN1:def 2;

then A29: rng h c= dom R ;

A30: n in NAT by ORDINAL1:def 12;

then ex x being Real st

( x in N & x in N1 & h . n = x - x0 ) by A21;

then (r * (h . n)) + (R . (h . n)) = (s * (h . n)) + (R1 . (h . n)) by A25;

then A31: ((r * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n)) = ((s * (h . n)) + (R1 . (h . n))) / (h . n) by XCMPLX_1:62;

A32: (R . (h . n)) / (h . n) = (R . (h . n)) * ((h . n) ") by XCMPLX_0:def 9

.= (R . (h . n)) * ((h ") . n) by VALUED_1:10

.= ((R /* h) . n) * ((h ") . n) by A30, A29, FUNCT_2:108

.= ((h ") (#) (R /* h)) . n by SEQ_1:8 ;

A33: h . n <> 0 by SEQ_1:5;

A34: (R1 . (h . n)) / (h . n) = (R1 . (h . n)) * ((h . n) ") by XCMPLX_0:def 9

.= (R1 . (h . n)) * ((h ") . n) by VALUED_1:10

.= ((R1 /* h) . n) * ((h ") . n) by A30, A28, FUNCT_2:108

.= ((h ") (#) (R1 /* h)) . n by SEQ_1:8 ;

A35: (s * (h . n)) / (h . n) = s * ((h . n) / (h . n)) by XCMPLX_1:74

.= s * 1 by A33, XCMPLX_1:60

.= s ;

(r * (h . n)) / (h . n) = r * ((h . n) / (h . n)) by XCMPLX_1:74

.= r * 1 by A33, XCMPLX_1:60

.= r ;

then r + ((R . (h . n)) / (h . n)) = s + ((R1 . (h . n)) / (h . n)) by A31, A35, XCMPLX_1:62;

then r = s + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)) by A32, A34;

hence rs = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n by RFUNCT_2:1; :: thesis: verum

then A36: lim (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) = r - s by SEQ_4:25;

A37: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 ) by Def2;

( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 ) by Def2;

then r - s = 0 - 0 by A36, A37, SEQ_2:12;

hence r = s ; :: thesis: verum