Bounds of real roots of a system of algebraic equations

Let $V\subset\mathbb R^n$ be real algebraic variety defined by the system of equations $f_1=\dots=f_m=0$, where $f_i\in\mathbb Q[x_1,\dots,x_n]$ $(i=1,2,\dots,n)$. Denote by $L$ the maximum of bitwise lengths of descriptions of coefficients of the system and propose $d=\sum_{i=1}^n\operatorname{deg}f_i$, $r=\binom{n+2d}n$. It is proved, that for any compound $V'$ of the variety $V$ there exists such a point $x=(x_1,\dots,x_n)\in V'$, that $|x_i|<2^{H(r,L)}(i=1,\dots,n)$, where $H$ – is a polynomial independent on the input system. If $V$ is compact, then any point $x\in V$ has the metnioned property. Such kind of bounds may appear useful for creating subexponential-time algorithm for finding the real roots of algebraic systems.
The idea of the proof is the approximation of the input system real roots by corresponding complex roots of a certain sequence of systems which have finite number of roots each. The constraction of this sequence in the case of a compact $V$ uses the technic from [б] and can be realized as follows. It is sufficient to consider real varieties defined by one equation $f=0$ (replacing $f$ by $\sum_{i=1}^mf_i^2$). If null is critical value of the function $f$, then consider the sequence of polynomials $\tilde f^{(l)}=f-\nu_l$, where $\nu_l\in\mathbb R$ $(l=1,2,\dots)$ are regular values of $f$ and $\lim_{l\to\infty}\nu_l=0$. If points $(0,\dots,0,\pm1)\in S^{n-1}$ are critical values of Gauss mappings of varieties $\{\tilde f^{(l)}=0\}$ then trasform the sequence proposing $f^{(l)}(x)=\tilde f^{(l)}(\tilde M^{(l)}x)$, where $M^{(l)} (l=1,2,\dots)$ are appropriativ rotation matrices and $(0,\dots,0,\pm1)$ – regular values of Gauss mappings of varieties $\{f^{(l)}=0\}$. Approximate polynomials $\partial f^{(l)}/\partial x_1,\dots,\partial f^{(l)}/\partial x_{n-1}, f$ by polynomials $g_1^{(l)},\dots,g_n^{(l)}$ of the same degrees with real algebraically independent coefficients. As a result we have the sought sequence of the systems: $g_1^{(l)}=\dots=g_n^{(l)}=0$ $(l=1,2,\dots)$. The case, when $V$ is not compact is treated analogously, with the help of induction on $n$. Bounds for limit roots of a sequence of systems are obtained in lemma 1 with the help of one theorem due to Lazard ([5]).
In §3 some lower bounds for coordinates of real roots are obtained as corollaries.