let r, s be Real; :: thesis: ( ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,(pdiff1 (f,1)),u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for z being Real st z in N holds
((SVF1 (3,(pdiff1 (f,1)),u)) . z) - ((SVF1 (3,(pdiff1 (f,1)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) & ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,(pdiff1 (f,1)),u)) & ex L being LinearFunc ex R being RestFunc st
( s = L . 1 & ( for z being Real st z in N holds
((SVF1 (3,(pdiff1 (f,1)),u)) . z) - ((SVF1 (3,(pdiff1 (f,1)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) implies r = s )
assume that
A6: ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,(pdiff1 (f,1)),u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for z being Real st z in N holds
((SVF1 (3,(pdiff1 (f,1)),u)) . z) - ((SVF1 (3,(pdiff1 (f,1)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) and
A7: ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,(pdiff1 (f,1)),u)) & ex L being LinearFunc ex R being RestFunc st
( s = L . 1 & ( for z being Real st z in N holds
((SVF1 (3,(pdiff1 (f,1)),u)) . z) - ((SVF1 (3,(pdiff1 (f,1)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) ; :: thesis: r = s
consider x0, y0, z0 being Real such that
A8: ( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,(pdiff1 (f,1)),u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for z being Real st z in N holds
((SVF1 (3,(pdiff1 (f,1)),u)) . z) - ((SVF1 (3,(pdiff1 (f,1)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) by A6;
consider N being Neighbourhood of z0 such that
A9: ( N c= dom (SVF1 (3,(pdiff1 (f,1)),u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for z being Real st z in N holds
((SVF1 (3,(pdiff1 (f,1)),u)) . z) - ((SVF1 (3,(pdiff1 (f,1)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) by A8;
consider L being LinearFunc, R being RestFunc such that
A10: ( r = L . 1 & ( for z being Real st z in N holds
((SVF1 (3,(pdiff1 (f,1)),u)) . z) - ((SVF1 (3,(pdiff1 (f,1)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) by A9;
consider x1, y1, z1 being Real such that
A11: ( u = <*x1,y1,z1*> & ex N being Neighbourhood of z1 st
( N c= dom (SVF1 (3,(pdiff1 (f,1)),u)) & ex L being LinearFunc ex R being RestFunc st
( s = L . 1 & ( for z being Real st z in N holds
((SVF1 (3,(pdiff1 (f,1)),u)) . z) - ((SVF1 (3,(pdiff1 (f,1)),u)) . z1) = (L . (z - z1)) + (R . (z - z1)) ) ) ) ) by A7;
consider N1 being Neighbourhood of z1 such that
A12: ( N1 c= dom (SVF1 (3,(pdiff1 (f,1)),u)) & ex L being LinearFunc ex R being RestFunc st
( s = L . 1 & ( for z being Real st z in N1 holds
((SVF1 (3,(pdiff1 (f,1)),u)) . z) - ((SVF1 (3,(pdiff1 (f,1)),u)) . z1) = (L . (z - z1)) + (R . (z - z1)) ) ) ) by A11;
consider L1 being LinearFunc, R1 being RestFunc such that
A13: ( s = L1 . 1 & ( for z being Real st z in N1 holds
((SVF1 (3,(pdiff1 (f,1)),u)) . z) - ((SVF1 (3,(pdiff1 (f,1)),u)) . z1) = (L1 . (z - z1)) + (R1 . (z - z1)) ) ) 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 :: thesis: for z being Real st z in N & z in N1 holds
(r * (z - z0)) + (R . (z - z0)) = (s * (z - z0)) + (R1 . (z - z0))
let z be Real; :: thesis: ( z in N & z in N1 implies (r * (z - z0)) + (R . (z - z0)) = (s * (z - z0)) + (R1 . (z - z0)) )
assume A20: ( z in N & z in N1 ) ; :: thesis: (r * (z - z0)) + (R . (z - z0)) = (s * (z - z0)) + (R1 . (z - z0))
then ((SVF1 (3,(pdiff1 (f,1)),u)) . z) - ((SVF1 (3,(pdiff1 (f,1)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) by A10;
then (L . (z - z0)) + (R . (z - z0)) = (L1 . (z - z0)) + (R1 . (z - z0)) by A13, A18, A20;
then (r1 * (z - z0)) + (R . (z - z0)) = (L1 . (z - z0)) + (R1 . (z - z0)) by A14;
hence (r * (z - z0)) + (R . (z - z0)) = (s * (z - z0)) + (R1 . (z - z0)) by A15, A16, A17; :: thesis: verum
end;
consider N0 being Neighbourhood of z0 such that
A21: ( N0 c= N & N0 c= N1 ) by A18, RCOMP_1:17;
consider g being Real such that
A22: ( 0 < g & N0 = ].(z0 - g),(z0 + 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();
now :: thesis: for n being Nat holds s1 . n <> 0
let n be Nat; :: thesis: s1 . n <> 0
g / (n + 2) <> 0 by A22, XREAL_1:139;
hence s1 . n <> 0 by A23; :: thesis: verum
end;
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 z being Real st
( z in N & z in N1 & h . n = z - z0 )
proof
let n be Element of NAT ; :: thesis: ex z being Real st
( z in N & z in N1 & h . n = z - z0 )
A26: g / (n + 2) > 0 by A22, XREAL_1:139;
0 + 1 < (n + 1) + 1 by XREAL_1:6;
then g / (n + 2) < g / 1 by A22, XREAL_1:76;
then A27: z0 + (g / (n + 2)) < z0 + g by XREAL_1:6;
z0 + (- g) < z0 + (g / (n + 2)) by A22, A26, XREAL_1:6;
then A28: z0 + (g / (n + 2)) in ].(z0 - g),(z0 + g).[ by A27;
take z0 + (g / (n + 2)) ; :: thesis: ( z0 + (g / (n + 2)) in N & z0 + (g / (n + 2)) in N1 & h . n = (z0 + (g / (n + 2))) - z0 )
thus ( z0 + (g / (n + 2)) in N & z0 + (g / (n + 2)) in N1 & h . n = (z0 + (g / (n + 2))) - z0 ) by A21, A22, A23, A28; :: thesis: verum
end;
A29: r - s in REAL by XREAL_0:def 1;
A30: now :: thesis: for n being Nat holds r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n
let n be Nat; :: thesis: r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n
A31: n in NAT by ORDINAL1:def 12;
then ex z being Real st
( z in N & z in N1 & h . n = z - z0 ) 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; :: thesis: 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 ; :: thesis: verum