\Ba{}~\\
Let $p = \sum_{i=1}^n f_i \rmult m_i$ with $n \in \n$, $f_i \in F$,
 $m_i \in \monoms(\f_{\myk})$
 be a right reductive standard  representation of $p$ in terms of $F$, i.e.,
 $\hterm(p) = \hterm(\hterm(f_1) \rmult m_1) =
 \hterm(f_1 \rmult m_1) \geq \hterm(f_1)$ and
 $\hterm(p) \succeq  \hterm(f_i \rmult m_i)$
 for all $2 \leq i \leq n$. 
\\
Let us first analyze $f_1 \rmult m_1 \rmult m$:\\
Let $\terms(f_1 \rmult m_1) = \{ s_1, \ldots, s_k \}$ with $s_1 \succ s_i$, $2 \leq i \leq k$,
 i.e.~$s_1 = \hterm(f_1 \rmult m_1) = \hterm(\hterm(f_1) \rmult m_1) = \hterm(p)$.
Hence $\hterm(p) \rmult m = s_1 \rmult m \geq \hterm(p) = s_1$ and as $s_1 \succ s_i$,
 $2 \leq i \leq k$, by Definition \ref{def.refined.ordering} we can conclude
 $\hterm(\hterm(p) \rmult m) 
 = \hterm(s_1 \rmult m) \succ s_i \rmult m \succeq \hterm(s_i \rmult m)$
 for $2 \leq i \leq k$.
This implies $\hterm(\hterm(f_1 \rmult m_1) \rmult m) = \hterm(f_1 \rmult m_1 \rmult m)$.
Hence we get
\begin{eqnarray*}
 \hterm(p \rmult m) & = & \hterm(\hterm(p) \rmult m) \\
                    & = & \hterm(\hterm(f_1 \rmult m_1) \rmult m), \mbox{ as } 
                          \hterm(p) = \hterm(f_1 \rmult m_1) \\
                    & = & \hterm(f_1 \rmult m_1 \rmult m)
\end{eqnarray*}
and
since $\hterm(p \rmult m) \geq \hterm(p) \geq \hterm(f_1)$ we can conclude
 $\hterm(f_1 \rmult m_1 \rmult m) \geq \hterm(f_1)$.
It remains to show that $f_1 \rmult m_1 \rmult m$ has
 a right reductive standard representation in terms of $F$.
First we show that $\hterm(\hterm(f_1) \rmult m_1 \rmult m) \geq \hterm(f_1)$.
%alt
%Let $\terms (f_1) = \{ t_1, \ldots, t_l \}$ with $t_1 \succ t_i$,  $2 \leq i \leq l$,
% i.e.~$t_1 = \hterm(f_1)$.
%As $\hterm( \hterm(f_1) \rmult m_1) \geq \hterm(f_1) \succ t_i$,$2 \leq i \leq l$,
% we get $\hterm(\hterm(f_1) \rmult m_1) \succ t_i \rmult m_1 \succeq \hterm(t_i \rmult m_1)$,
% and $\hterm(f_1) \rmult m_1 \succ \sum_{i=2}^l t_i \rmult m_1$.
%Moreover, $\hterm(f_1) \rmult m_1 \succeq 
% \hterm(\hterm(f_1) \rmult m_1) = \hterm(f_1 \rmult m_1)$\footnote{Notice that
% $\hterm(f_1) \rmult m_1$ can be a polynomial and hence we cannot conclude 
% $\hterm(f_1) \rmult m_1 = \hterm(\hterm(f_1) \rmult m_1)$.}
% since $f_1 \rmult m_1 = \sum_{i=1}^l t_i \rmult m_1$.
%Hence $\hterm(\hterm(f_1 \rmult m_1) \rmult m) = \hterm(\hterm(f_1) \rmult m_1 \rmult m) \geq \hterm(f_1)$.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%neu
We know $\hterm(f_1) \rmult m_1 \succeq 
 \hterm(\hterm(f_1) \rmult m_1) = \hterm(f_1 \rmult m_1)$\footnote{Notice that
 $\hterm(f_1) \rmult m_1$ can be a polynomial and hence we cannot conclude 
 $\hterm(f_1) \rmult m_1 = \hterm(\hterm(f_1) \rmult m_1)$.}
 and hence
 $\hterm(\hterm(f_1) \rmult m_1 \rmult m) = \hterm(\hterm(f_1 \rmult m_1) \rmult m) =
  \hterm(f_1 \rmult m_1 \rmult m) \geq \hterm(f_1)$.
\\
%Weiter
Now in case $m_1 \rmult m \in \monoms(\f_{\myk})$ we are done as then $f_1 \rmult ( m_1 \rmult m)$
 is a right reductive standard representation in terms of $F$.
\\
Hence let us assume
 $m_1 \rmult m = \sum_{j=1}^{k} \tilde{m}_j$, $\tilde{m}_j \in \monoms(\f_{\myk})$.
Let $\terms (f_1) = \{ t_1, \ldots, t_l \}$ with $t_1 \succ t_l$,  $2 \leq l \leq s$,
 i.e.~$t_1 = \hterm(f_1)$.
As $\hterm( \hterm(f_1) \rmult m_1) \geq \hterm(f_1) \succ t_l$,$2 \leq l \leq s$,
 again by Definition \ref{def.refined.ordering}
 we can conclude $\hterm(\hterm(f_1) \rmult m_1) \succ t_l \rmult m_1 \succeq \hterm(t_l \rmult m_1)$,
 and $\hterm(f_1) \rmult m_1 \succ \sum_{l=2}^s t_l \rmult m_1$.
Then for each $s_i$, $2 \leq i \leq k$
 there exists $t_l \in \terms(f_1)$ such that
 $s_i \in \supp(t_l \rmult m_1)$.
Since $\hterm(p) \succ s_i$ and even\footnote{$\hterm(p) \succ t_l \rmult m_1$
 if $\hterm(f_1 \rmult m_1) \not\in \supp(t_l \rmult m_1)$.}
 $\hterm(p) \succeq t_l \rmult m_1$ we find that
 either
 $\hterm(p \rmult m) \succeq \hterm((t_l \rmult m_1) \rmult m) = \hterm(t_l \rmult (m_1 \rmult m))$
 in case $\hterm(t_l \rmult m_1 ) = \hterm(f_1 \rmult m_1)$
 or 
 $\hterm(p \rmult m) \succ \hterm(t_l \rmult m_1) \rmult m) = \hterm(t_l \rmult (m_1 \rmult m))$.
Hence we can conclude $f_1 \rmult \tilde{m}_j \predeq \hterm(p \rmult m)$, $1 \leq j \leq k$ and
 for at least one $\tilde{m}_j$ we get
 $\hterm(f_1 \rmult \tilde{m}_j) = \hterm(f_1 \rmult m_1 \rmult m) \geq \hterm(f_1)$.
\\
It remains to analyze the situation for the function
 $(\sum_{i=2}^n f_i \rmult m_i) \rmult m$.
Again we find that for all terms $s$ in the $f_i \rmult m_i$, $2 \leq i \leq n$,
 we have $\hterm(p) \succeq s$ and we get 
 $\hterm(p \rmult m) \succeq \hterm(s \rmult m)$.
Hence all polynomial multiples of the $f_i$  in the representation 
 $\sum_{i=2}^n \sum_{j=1}^{k_i} f_i \rmult \tilde{m}^i_j$, where
 $m_i \rmult m = \sum_{j=1}^{k_i}\tilde{m}^i_j$, are bounded by 
 $\hterm(p \rmult m)$.
\\
\qed