let r, s be Real; ( ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) & ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( s = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) implies r = s )
assume that
A8:
ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) )
and
A9:
ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( s = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) )
; r = s
consider x1, y1 being Real such that
A10:
z = <*x1,y1*>
and
A11:
ex N being Neighbourhood of x1 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( s = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x1) = (L . (x - x1)) + (R . (x - x1)) ) ) )
by A9;
consider N1 being Neighbourhood of x1 such that
N1 c= dom (SVF1 (1,(pdiff1 (f,2)),z))
and
A12:
ex L being LinearFunc ex R being RestFunc st
( s = L . 1 & ( for x being Real st x in N1 holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x1) = (L . (x - x1)) + (R . (x - x1)) ) )
by A11;
consider L1 being LinearFunc, R1 being RestFunc such that
A13:
s = L1 . 1
and
A14:
for x being Real st x in N1 holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x1) = (L1 . (x - x1)) + (R1 . (x - x1))
by A12;
consider p1 being Real such that
A15:
for p being Real holds L1 . p = p1 * p
by FDIFF_1:def 3;
A16:
s = p1 * 1
by A13, A15;
consider x0, y0 being Real such that
A17:
z = <*x0,y0*>
and
A18:
ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) )
by A8;
consider N being Neighbourhood of x0 such that
N c= dom (SVF1 (1,(pdiff1 (f,2)),z))
and
A19:
ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) )
by A18;
consider L being LinearFunc, R being RestFunc such that
A20:
r = L . 1
and
A21:
for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0))
by A19;
consider r1 being Real such that
A22:
for p being Real holds L . p = r1 * p
by FDIFF_1:def 3;
A23:
x0 = x1
by A17, A10, FINSEQ_1:77;
then consider N0 being Neighbourhood of x0 such that
A24:
( N0 c= N & N0 c= N1 )
by RCOMP_1:17;
consider g being Real such that
A25:
0 < g
and
A26:
N0 = ].(x0 - g),(x0 + g).[
by RCOMP_1:def 6;
deffunc H1( Nat) -> set = g / ($1 + 2);
consider s1 being Real_Sequence such that
A27:
for n being Nat holds s1 . n = H1(n)
from SEQ_1:sch 1();
then A28:
s1 is non-zero
by SEQ_1:5;
( s1 is convergent & lim s1 = 0 )
by A27, SEQ_4:31;
then reconsider h = s1 as non-zero 0 -convergent Real_Sequence by A28, FDIFF_1:def 1;
A29:
for n being Element of NAT ex x being Real st
( x in N & x in N1 & h . n = x - x0 )
A31:
r = r1 * 1
by A20, A22;
A32:
now for x being Real st x in N & x in N1 holds
(r * (x - x0)) + (R . (x - x0)) = (s * (x - x0)) + (R1 . (x - x0))let x be
Real;
( x in N & x in N1 implies (r * (x - x0)) + (R . (x - x0)) = (s * (x - x0)) + (R1 . (x - x0)) )assume that A33:
x in N
and A34:
x in N1
;
(r * (x - x0)) + (R . (x - x0)) = (s * (x - x0)) + (R1 . (x - x0))
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0))
by A21, A33;
then
(L . (x - x0)) + (R . (x - x0)) = (L1 . (x - x0)) + (R1 . (x - x0))
by A14, A23, A34;
then
(r1 * (x - x0)) + (R . (x - x0)) = (L1 . (x - x0)) + (R1 . (x - x0))
by A22;
hence
(r * (x - x0)) + (R . (x - x0)) = (s * (x - x0)) + (R1 . (x - x0))
by A15, A31, A16;
verum end;
A35:
r - s in REAL
by XREAL_0:def 1;
now for n being Nat holds r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n
dom R1 = REAL
by PARTFUN1:def 2;
then A36:
rng h c= dom R1
;
let n be
Nat;
r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n
dom R = REAL
by PARTFUN1:def 2;
then A37:
rng h c= dom R
;
A38:
n in NAT
by ORDINAL1:def 12;
then
ex
x being
Real st
(
x in N &
x in N1 &
h . n = x - x0 )
by A29;
then
(r * (h . n)) + (R . (h . n)) = (s * (h . n)) + (R1 . (h . n))
by A32;
then A39:
((r * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n)) = ((s * (h . n)) + (R1 . (h . n))) / (h . n)
by XCMPLX_1:62;
A40:
(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 A38, A37, FUNCT_2:108
.=
((h ") (#) (R /* h)) . n
by VALUED_1:5
;
A41:
h . n <> 0
by SEQ_1:5;
A42:
(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 A38, A36, FUNCT_2:108
.=
((h ") (#) (R1 /* h)) . n
by VALUED_1:5
;
A43:
(s * (h . n)) / (h . n) =
s * ((h . n) / (h . n))
by XCMPLX_1:74
.=
s * 1
by A41, XCMPLX_1:60
.=
s
;
(r * (h . n)) / (h . n) =
r * ((h . n) / (h . n))
by XCMPLX_1:74
.=
r * 1
by A41, XCMPLX_1:60
.=
r
;
then
r + ((R . (h . n)) / (h . n)) = s + ((R1 . (h . n)) / (h . n))
by A39, A43, XCMPLX_1:62;
then
r = s + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n))
by A40, A42;
hence
r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n
by A38, VALUED_1:15;
verum end;
then
( ((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h)) is constant & (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . 1 = r - s )
by VALUED_0:def 18, A35;
then A44:
lim (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) = r - s
by SEQ_4:25;
A45:
( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 )
by FDIFF_1:def 2;
( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 )
by FDIFF_1:def 2;
then
r - s = 0 - 0
by A44, A45, SEQ_2:12;
hence
r = s
; verum