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 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 abs 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 abs h < d & h <> 0 & (h * z) + x0 in N1 holds
||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - dv1).|| < e ) ) by A2;

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 A5;
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 A4, 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

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 3;
consider n0 being Element of NAT such that
A15: ||.z.|| / g < n0 by SEQ_4:10;
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:
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:217;
A19: 0 <= n0 by NAT_1:2;
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 A18, XXREAL_0:15; :: thesis:
A21: 0 < min (1 / ((n0 + 1) + 1)),((min d1,d2) / 2) by A18, A20, 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:70;
then ||.z.|| < (n0 + 1) * g by A13, XCMPLX_1:88;
then A22: ||.z.|| / (n0 + 1) < g by A19, XREAL_1:85;
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 ;
A24: (min d1,d2) / 2 < min d1,d2 by A17, XREAL_1:218;
min d1,d2 <= d2 by XXREAL_0:17;
then (min d1,d2) / 2 < d2 by A24, XXREAL_0:2;
then A25: 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 A24, XXREAL_0:2;
then min (1 / ((n0 + 1) + 1)),((min d1,d2) / 2) < d1 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, A25, ABSVALUE:def 1; :: thesis:
0 <= ||.z.|| by NORMSP_1:8;
then A26: (min (1 / ((n0 + 1) + 1)),((min d1,d2) / 2)) * ||.z.|| <= (1 / ((n0 + 1) + 1)) * ||.z.|| by XREAL_1:66, XXREAL_0:17;
( 0 <= ||.z.|| & n0 + 1 <= 1 + (n0 + 1) ) by NAT_1:12, NORMSP_1:8;
then A27: ||.z.|| / (1 + (n0 + 1)) <= ||.z.|| / (n0 + 1) by A19, XREAL_1:120;
(1 / (1 + (n0 + 1))) * ||.z.|| = ||.z.|| / (1 + (n0 + 1)) by XCMPLX_1:100;
then (1 / (1 + (n0 + 1))) * ||.z.|| < g by A22, A27, XXREAL_0:2;
then ||.((((min (1 / ((n0 + 1) + 1)),((min d1,d2) / 2)) * z) + x0) - x0).|| < g by A23, A26, 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:

end;

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

end;

hence dv1 = dv2 by Th4; :: thesis: