let dv1, dv2 be Point of T; :: thesis: ( ex N being Neighbourhood of x0 st
( N c= dom f & ( for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st |.h.| < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv1).|| < e ) ) ) ) & ex N being Neighbourhood of x0 st
( N c= dom f & ( for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st |.h.| < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv2).|| < e ) ) ) ) implies dv1 = dv2 )
assume that
A2: ex N1 being Neighbourhood of x0 st
( N1 c= dom f & ( for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st |.h.| < d & h <> 0 & (h * z) + x0 in N1 holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv1).|| < e ) ) ) ) and
A3: ex N2 being Neighbourhood of x0 st
( N2 c= dom f & ( for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st |.h.| < d & h <> 0 & (h * z) + x0 in N2 holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv2).|| < e ) ) ) ) ; :: thesis: dv1 = dv2
consider N2 being Neighbourhood of x0 such that
N2 c= dom f and
A4: for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st |.h.| < d & h <> 0 & (h * z) + x0 in N2 holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv2).|| < e ) ) by A3;
consider N1 being Neighbourhood of x0 such that
N1 c= dom f and
A5: for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st |.h.| < d & h <> 0 & (h * z) + x0 in N1 holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv1).|| < e ) ) by A2;

now :: thesis: for e being Real st e > 0 holds
||.(dv1 - dv2).|| < e

let e be Real; :: thesis: ( e > 0 implies ||.(dv1 - dv2).|| < e )
assume A6: e > 0 ; :: thesis: ||.(dv1 - dv2).|| < e
A7: 0 < e / 2 by A6, XREAL_1:215;
then consider d1 being Real such that
A8: d1 > 0 and
A9: for h being Real st |.h.| < d1 & h <> 0 & (h * z) + x0 in N1 holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv1).|| < e / 2 by A5;
consider d2 being Real such that
A10: d2 > 0 and
A11: for h being Real st |.h.| < d2 & h <> 0 & (h * z) + x0 in N2 holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv2).|| < e / 2 by A4, A7;
ex h being Real st
( h <> 0 & |.h.| < d1 & |.h.| < d2 & (h * z) + x0 in N1 & (h * z) + x0 in N2 )

proof

set d3 = min (d1,d2);
consider N0 being Neighbourhood of x0 such that
A12: ( N0 c= N1 & N0 c= N2 ) by NDIFF_1:1;
consider g being Real such that
A13: 0 < g and
A14: { y where y is Point of S : ||.(y - x0).|| < g } c= N0 by NFCONT_1:def 1;
consider n0 being Nat such that
A15: ||.z.|| / g < n0 by SEQ_4:3;
set n1 = n0 + 1;
set h = min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2));
take min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2)) ; :: thesis: ( min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2)) <> 0 & |.(min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))).| < d1 & |.(min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))).| < d2 & ((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + x0 in N1 & ((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + x0 in N2 )
A16: min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2)) <= (min (d1,d2)) / 2 by XXREAL_0:17;
A17: 0 < min (d1,d2) by A8, A10, XXREAL_0:15;
then A18: 0 < (min (d1,d2)) / 2 by XREAL_1:215;
0 < 1 * ((1 + (n0 + 1)) ") ;
then A19: 0 < 1 / (1 + (n0 + 1)) by XCMPLX_0:def 9;
hence min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2)) <> 0 by A18, XXREAL_0:15; :: thesis: ( |.(min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))).| < d1 & |.(min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))).| < d2 & ((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + x0 in N1 & ((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + x0 in N2 )
A20: 0 < min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2)) by A18, A19, XXREAL_0:15;
n0 <= n0 + 1 by NAT_1:11;
then ||.z.|| / g < n0 + 1 by A15, XXREAL_0:2;
then (||.z.|| / g) * g < (n0 + 1) * g by A13, XREAL_1:68;
then ||.z.|| < (n0 + 1) * g by A13, XCMPLX_1:87;
then A21: ||.z.|| / (n0 + 1) < g by XREAL_1:83;
A22: ||.((((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + x0) - x0).|| = ||.(((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + (x0 - x0)).|| by RLVECT_1:def 3
.= ||.(((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + (0. S)).|| by RLVECT_1:15
.= ||.((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z).|| by RLVECT_1:4
.= |.(min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))).| * ||.z.|| by NORMSP_1:def 1
.= (min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * ||.z.|| by A20, ABSVALUE:def 1 ;
A23: (min (d1,d2)) / 2 < min (d1,d2) by A17, XREAL_1:216;
min (d1,d2) <= d2 by XXREAL_0:17;
then (min (d1,d2)) / 2 < d2 by A23, XXREAL_0:2;
then A24: min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2)) < d2 by A16, XXREAL_0:2;
min (d1,d2) <= d1 by XXREAL_0:17;
then (min (d1,d2)) / 2 < d1 by A23, XXREAL_0:2;
then min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2)) < d1 by A16, XXREAL_0:2;
hence ( |.(min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))).| < d1 & |.(min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))).| < d2 ) by A20, A24, ABSVALUE:def 1; :: thesis: ( ((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + x0 in N1 & ((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + x0 in N2 )
0 <= ||.z.|| by NORMSP_1:4;
then A25: (min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * ||.z.|| <= (1 / ((n0 + 1) + 1)) * ||.z.|| by XREAL_1:64, XXREAL_0:17;
( 0 <= ||.z.|| & n0 + 1 <= 1 + (n0 + 1) ) by NAT_1:12, NORMSP_1:4;
then A26: ||.z.|| / (1 + (n0 + 1)) <= ||.z.|| / (n0 + 1) by XREAL_1:118;
(1 / (1 + (n0 + 1))) * ||.z.|| = ||.z.|| / (1 + (n0 + 1)) by XCMPLX_1:99;
then (1 / (1 + (n0 + 1))) * ||.z.|| < g by A21, A26, XXREAL_0:2;
then ||.((((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + x0) - x0).|| < g by A22, A25, XXREAL_0:2;
then ((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + x0 in { y where y is Point of S : ||.(y - x0).|| < g } ;
then ((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + x0 in N0 by A14;
hence ( ((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + x0 in N1 & ((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + x0 in N2 ) by A12; :: thesis: verum

end;

then consider h being Real such that
A27: |.h.| < d1 and
A28: |.h.| < d2 and
A29: h <> 0 and
A30: (h * z) + x0 in N1 and
A31: (h * z) + x0 in N2 ;
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv1).|| < e / 2 by A9, A27, A29, A30;
then A32: ||.(dv1 - ((h ") * ((f /. ((h * z) + x0)) - (f /. x0)))).|| < e / 2 by Th4;
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv2).|| < e / 2 by A11, A28, A29, A31;
hence ||.(dv1 - dv2).|| < e by A6, A32, Th4; :: thesis: verum

end;

hence dv1 = dv2 by Th4; :: thesis: verum