let r, s be Point of F; ( ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F 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 of F ex R being RestFunc of F 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 of F ex R being RestFunc of F 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 of F ex R being RestFunc of F st
( s = L /. 1 & ( for x being Real st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) ) )
; r = s
consider N being Neighbourhood of x0 such that
N c= dom f
and
A8:
ex L being LinearFunc of F ex R being RestFunc of F 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 of F, R being RestFunc of F 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 Point of F such that
A11:
for p being Real holds L /. p = p * r1
by Def2;
consider N1 being Neighbourhood of x0 such that
N1 c= dom f
and
A12:
ex L being LinearFunc of F ex R being RestFunc of F 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 of F, R1 being RestFunc of F 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 Point of F such that
A15:
for p being Real holds L1 /. p = p * p1
by Def2;
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 H1( Nat) -> set = g / ($1 + 2);
consider s1 being Real_Sequence such that
A19:
for n being Nat holds s1 . n = H1(n)
from SEQ_1:sch 1();
then A20:
s1 is non-zero
by SEQ_1:5;
( s1 is convergent & lim s1 = 0 )
by A19, SEQ_4:31;
then reconsider h = s1 as non-zero 0 -convergent Real_Sequence by A20, FDIFF_1:def 1;
A21:
for n being Element of NAT ex x being Real st
( x in N & x in N1 & h . n = x - x0 )
A23:
s = 1 * p1
by A13, A15;
A24:
r = 1 * r1
by A9, A11;
A25:
now for x being Real st x in N & x in N1 holds
((x - x0) * r) + (R /. (x - x0)) = ((x - x0) * s) + (R1 /. (x - x0))end;
now for n being Nat holds r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n
R1 is
total
by Def1;
then
dom R1 = REAL
by PARTFUN1:def 2;
then A28:
rng h c= dom R1
;
let n be
Nat;
r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n
R is
total
by Def1;
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
((h . n) * r) + (R /. (h . n)) = ((h . n) * s) + (R1 /. (h . n))
by A25;
then
((1 / (h . n)) * ((h . n) * r)) + ((1 / (h . n)) * (R /. (h . n))) = (1 / (h . n)) * (((h . n) * s) + (R1 /. (h . n)))
by RLVECT_1:def 5;
then
(((1 / (h . n)) * (h . n)) * r) + ((1 / (h . n)) * (R /. (h . n))) = (1 / (h . n)) * (((h . n) * s) + (R1 /. (h . n)))
by RLVECT_1:def 7;
then A31:
(((1 / (h . n)) * (h . n)) * r) + ((1 / (h . n)) * (R /. (h . n))) = ((1 / (h . n)) * ((h . n) * s)) + ((1 / (h . n)) * (R1 /. (h . n)))
by RLVECT_1:def 5;
A32:
(1 / (h . n)) * (R /. (h . n)) =
((h . n) ") * (R /. (h . n))
by XCMPLX_1:215
.=
((h ") . n) * (R /. (h . n))
by VALUED_1:10
.=
((h ") . n) * ((R /* h) . n)
by A30, A29, FUNCT_2:109
.=
((h ") (#) (R /* h)) . n
by NDIFF_1:def 2
;
A33:
h . n <> 0
by SEQ_1:5;
A34:
(1 / (h . n)) * (R1 /. (h . n)) =
((h . n) ") * (R1 /. (h . n))
by XCMPLX_1:215
.=
((h ") . n) * (R1 /. (h . n))
by VALUED_1:10
.=
((h ") . n) * ((R1 /* h) . n)
by A30, A28, FUNCT_2:109
.=
((h ") (#) (R1 /* h)) . n
by NDIFF_1:def 2
;
A35:
((1 / (h . n)) * (h . n)) * s =
1
* s
by A33, XCMPLX_1:106
.=
s
by RLVECT_1:def 8
;
((1 / (h . n)) * (h . n)) * r =
1
* r
by A33, XCMPLX_1:106
.=
r
by RLVECT_1:def 8
;
then
r + (((h ") (#) (R /* h)) . n) = s + (((h ") (#) (R1 /* h)) . n)
by A31, A35, A32, A34, RLVECT_1:def 7;
then
r + ((((h ") (#) (R /* h)) . n) - (((h ") (#) (R /* h)) . n)) = (s + (((h ") (#) (R1 /* h)) . n)) - (((h ") (#) (R /* h)) . n)
by RLVECT_1:28;
then
r + ((((h ") (#) (R /* h)) . n) - (((h ") (#) (R /* h)) . n)) = s + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n))
by RLVECT_1:28;
then
r + (0. F) = s + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n))
by RLVECT_1:15;
then
r = s + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n))
by RLVECT_1:4;
then
r - s = ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)) + (s - s)
by RLVECT_1:28;
then
r - s = ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)) + (0. F)
by RLVECT_1:15;
then A36:
r - s = (((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)
by RLVECT_1:4;
thus
r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n
by A36, NORMSP_1:def 3;
verum end;
then
( ((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h)) is constant & (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . 0 = r - s )
by VALUED_0:def 18;
then A37:
lim (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) = r - s
by NDIFF_1:18;
A38:
( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0. F )
by Def1;
( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0. F )
by Def1;
then
r - s = (0. F) - (0. F)
by A37, A38, NORMSP_1:26;
hence
r = s
by RLVECT_1:13, RLVECT_1:21; verum