let dv1, dv2 be Point of T; :: thesis:
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 abs 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 abs h < d & h <> 0 & (h * z) + x0 in N2 holds
||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - dv2).|| < e ) ) ) ) ; :: thesis:
consider N1 being Neighbourhood of x0 such that
N1 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 abs h < d & h <> 0 & (h * z) + x0 in N1 holds
||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - dv1).|| < e ) ) by A2;
consider N2 being Neighbourhood of x0 such that
N2 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 abs h < d & h <> 0 & (h * z) + x0 in N2 holds
||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - dv2).|| < e ) ) by A3;

now

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

proof

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 & { y where y is Point of S : ||.(y - x0).|| < g } c= N0 ) by NFCONT_1:def 3;
set d3 = min d1,d2;
A14: ( min d1,d2 <= d1 & min d1,d2 <= d2 ) by XXREAL_0:17;
0 < min d1,d2 by A8, A10, XXREAL_0:15;
then A15: ( 0 < (min d1,d2) / 2 & (min d1,d2) / 2 < min d1,d2 ) by XREAL_1:217, XREAL_1:218;
then A16: ( (min d1,d2) / 2 < d1 & (min d1,d2) / 2 < d2 ) by A14, XXREAL_0:2;
consider n0 being Element of NAT such that
A17: ||.z.|| / g < n0 by SEQ_4:10;
0 <= n0 by NAT_1:2;
then A18: 0 < n0 + 1 ;
n0 <= n0 + 1 by NAT_1:11;
then ||.z.|| / g < n0 + 1 by A17, XXREAL_0:2;
then (||.z.|| / g) * g < (n0 + 1) * g by A13, XREAL_1:70;
then ||.z.|| < (n0 + 1) * g by A13, XCMPLX_1:88;
then A19: ||.z.|| / (n0 + 1) < g by A18, XREAL_1:85;
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:
0 + 0 < (n0 + 1) + 1 by A18;
then 0 < 1 * ((1 + (n0 + 1)) " ) ;
then A20: 0 < 1 / (1 + (n0 + 1)) by XCMPLX_0:def 9;
hence min (1 / ((n0 + 1) + 1)),((min d1,d2) / 2) <> 0 by A15, XXREAL_0:15; :: thesis:
A21: 0 < min (1 / ((n0 + 1) + 1)),((min d1,d2) / 2) by A15, A20, XXREAL_0:15;
( min (1 / ((n0 + 1) + 1)),((min d1,d2) / 2) <= 1 / ((n0 + 1) + 1) & min (1 / ((n0 + 1) + 1)),((min d1,d2) / 2) <= (min d1,d2) / 2 ) by XXREAL_0:17;
then ( min (1 / ((n0 + 1) + 1)),((min d1,d2) / 2) < d1 & min (1 / ((n0 + 1) + 1)),((min d1,d2) / 2) < d2 ) by A16, XXREAL_0:2;
hence ( abs (min (1 / ((n0 + 1) + 1)),((min d1,d2) / 2)) < d1 & abs (min (1 / ((n0 + 1) + 1)),((min d1,d2) / 2)) < d2 ) by A21, ABSVALUE:def 1; :: thesis:
( 0 <= ||.z.|| & n0 + 1 <= 1 + (n0 + 1) ) by NAT_1:12, NORMSP_1:8;
then A22: ||.z.|| / (1 + (n0 + 1)) <= ||.z.|| / (n0 + 1) by A18, XREAL_1:120;
A23: ||.((((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 6
.= ||.(((min (1 / ((n0 + 1) + 1)),((min d1,d2) / 2)) * z) + (0. S)).|| by RLVECT_1:28
.= ||.((min (1 / ((n0 + 1) + 1)),((min d1,d2) / 2)) * z).|| by RLVECT_1:10
.= (abs (min (1 / ((n0 + 1) + 1)),((min d1,d2) / 2))) * ||.z.|| by NORMSP_1:def 2
.= (min (1 / ((n0 + 1) + 1)),((min d1,d2) / 2)) * ||.z.|| by A21, ABSVALUE:def 1 ;
(1 / (1 + (n0 + 1))) * ||.z.|| = ||.z.|| / (1 + (n0 + 1)) by XCMPLX_1:100;
then A24: (1 / (1 + (n0 + 1))) * ||.z.|| < g by A19, A22, XXREAL_0:2;
( 0 <= ||.z.|| & min (1 / ((n0 + 1) + 1)),((min d1,d2) / 2) <= 1 / ((n0 + 1) + 1) ) by NORMSP_1:8, XXREAL_0:17;
then (min (1 / ((n0 + 1) + 1)),((min d1,d2) / 2)) * ||.z.|| <= (1 / ((n0 + 1) + 1)) * ||.z.|| by XREAL_1:66;
then ||.((((min (1 / ((n0 + 1) + 1)),((min d1,d2) / 2)) * z) + x0) - x0).|| < g by A23, A24, 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 A13;
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:

end;

then consider h being Real such that
A25: ( abs h < d1 & abs h < d2 & h <> 0 & (h * z) + x0 in N1 & (h * z) + x0 in N2 ) ;
A26: ||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - dv1).|| < e / 2 by A9, A25;
A27: ||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - dv2).|| < e / 2 by A11, A25;
||.(dv1 - ((h " ) * ((f /. ((h * z) + x0)) - (f /. x0)))).|| < e / 2 by A26, Th4;
hence ||.(dv1 - dv2).|| < e by A6, A27, Th4; :: thesis:

end;

hence dv1 = dv2 by Th4; :: thesis: