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