let r, s be Real; :: thesis: ( ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LINEAR ex R being REST 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 LINEAR ex R being REST 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
A5: ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LINEAR ex R being REST st
( r = L . 1 & ( for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) and
A6: ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LINEAR ex R being REST 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
A7: ( N c= dom f & ex L being LINEAR ex R being REST st
( r = L . 1 & ( for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) by A5;
consider L being LINEAR, R being REST such that
A8: ( r = L . 1 & ( for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by A7;
consider N1 being Neighbourhood of x0 such that
A9: ( N1 c= dom f & ex L being LINEAR ex R being REST st
( s = L . 1 & ( for x being Real st x in N1 holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) by A6;
consider L1 being LINEAR, R1 being REST such that
A10: ( s = L1 . 1 & ( for x being Real st x in N1 holds
(f . x) - (f . x0) = (L1 . (x - x0)) + (R1 . (x - x0)) ) ) by A9;
consider r1 being Real such that
A11: for p being Real holds L . p = r1 * p by Def4;
consider p1 being Real such that
A12: for p being Real holds L1 . p = p1 * p by Def4;
A13: r = r1 * 1 by A8, A11;
A14: s = p1 * 1 by A10, A12;
A15: now
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 A16: ( x in N & x in N1 ) ; :: thesis: (r * (x - x0)) + (R . (x - x0)) = (s * (x - x0)) + (R1 . (x - x0))
then (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A8;
then (L . (x - x0)) + (R . (x - x0)) = (L1 . (x - x0)) + (R1 . (x - x0)) by A10, A16;
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 A12, A13, A14; :: thesis: verum
end;
consider N0 being Neighbourhood of x0 such that
A17: ( N0 c= N & N0 c= N1 ) by RCOMP_1:38;
consider g being real number such that
A18: ( 0 < g & N0 = ].(x0 - g),(x0 + g).[ ) by RCOMP_1:def 7;
deffunc H1( Element of NAT ) -> Element of REAL = g / ($1 + 2);
consider s1 being Real_Sequence such that
A19: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch 1();
now
let n be Element of NAT ; :: thesis: 0 <> s1 . n
0 <> g / (n + 2) by A18, XREAL_1:141;
hence 0 <> s1 . n by A19; :: thesis: verum
end;
then A20: s1 is non-zero by SEQ_1:7;
( s1 is convergent & lim s1 = 0 ) by A19, SEQ_4:46;
then reconsider h = s1 as convergent_to_0 Real_Sequence by A20, Def1;
A21: for n being Element of NAT ex x being Real st
( x in N & x in N1 & h . n = x - x0 )
proof
let n be Element of NAT ; :: thesis: ex x being Real st
( x in N & x in N1 & h . n = x - x0 )
A22: 0 < g / (n + 2) by A18, XREAL_1:141;
0 + 1 < (n + 1) + 1 by XREAL_1:8;
then g / (n + 2) < g / 1 by A18, XREAL_1:78;
then A23: x0 + (g / (n + 2)) < x0 + g by XREAL_1:8;
x0 + (- g) < x0 + (g / (n + 2)) by A22, A18, XREAL_1:8;
then A24: x0 + (g / (n + 2)) in ].(x0 - g),(x0 + g).[ by A23;
take x = x0 + (g / (n + 2)); :: thesis: ( x in N & x in N1 & h . n = x - x0 )
thus ( x in N & x in N1 & h . n = x - x0 ) by A17, A18, A19, A24; :: thesis: verum
end;
A25: now
let n be Nat; :: thesis: r - s = (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) . n
X: n in NAT by ORDINAL1:def 13;
then ex x being Real st
( x in N & x in N1 & h . n = x - x0 ) by A21;
then A26: (r * (h . n)) + (R . (h . n)) = (s * (h . n)) + (R1 . (h . n)) by A15;
h is non-zero by Def1;
then A27: h . n <> 0 by X, SEQ_1:7;
A28: ((r * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n)) = ((s * (h . n)) + (R1 . (h . n))) / (h . n) by A26, XCMPLX_1:63;
A29: (r * (h . n)) / (h . n) = r * ((h . n) / (h . n)) by XCMPLX_1:75
.= r * 1 by A27, XCMPLX_1:60
.= r ;
(s * (h . n)) / (h . n) = s * ((h . n) / (h . n)) by XCMPLX_1:75
.= s * 1 by A27, XCMPLX_1:60
.= s ;
then A30: r + ((R . (h . n)) / (h . n)) = s + ((R1 . (h . n)) / (h . n)) by A28, A29, XCMPLX_1:63;
R is total by Def3;
then dom R = REAL by PARTFUN1:def 4;
then A31: rng h c= dom R ;
R1 is total by Def3;
then dom R1 = REAL by PARTFUN1:def 4;
then A32: rng h c= dom R1 ;
A33: (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 A31, X, FUNCT_2:185
.= ((h " ) (#) (R /* h)) . n by X, SEQ_1:12 ;
(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 A32, X, FUNCT_2:185
.= ((h " ) (#) (R1 /* h)) . n by X, SEQ_1:12 ;
then r = s + ((((h " ) (#) (R1 /* h)) . n) - (((h " ) (#) (R /* h)) . n)) by A30, A33;
hence r - s = (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) . n by X, RFUNCT_2:6; :: thesis: verum
end;
then A34: ((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h)) is V8() by VALUED_0:def 18;
(((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) . 1 = r - s by A25;
then A35: lim (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) = r - s by A34, SEQ_4:40;
A36: ( (h " ) (#) (R /* h) is convergent & lim ((h " ) (#) (R /* h)) = 0 ) by Def3;
( (h " ) (#) (R1 /* h) is convergent & lim ((h " ) (#) (R1 /* h)) = 0 ) by Def3;
then r - s = 0 - 0 by A35, A36, SEQ_2:26;
hence r = s ; :: thesis: verum