--- a/proof.tex	Fri Oct 12 05:45:48 2012 +0100
+++ b/proof.tex	Sun Oct 14 23:41:49 2012 +0100
@@ -105,7 +105,12 @@
 $d \not=c$: We have $der\,c\,d = \varnothing$.
 We also have $Der\,c\,\{\texttt{"}d\texttt{"}\} = \varnothing$. Hence we have 
 $\varnothing = \varnothing$  in (c). 
+\end{itemize}
 
+\noindent
+These were the easy base cases. Now come the inductive cases.
+
+\begin{itemize}
 \item Fourth Case: $P(r_1 + r_2)$ is $L(der\,c\,(r_1 + r_2)) = Der\,c\,(L(r_1 + r_2))$ (d). This is what we have to show.
 We can assume already:
 
@@ -169,9 +174,34 @@
 
 Similarly in the case where $r_1$ is \emph{not} nullable.
 
-\item Sixth Case:
+\item Sixth Case: $P(r^*)$ is $L(der\,c\,(r^*)) = Der\,c\,L(r^*)$. We can assume already:
+
+\begin{center}
+\begin{tabular}{ll}
+$P(r)$: & $L(der\,c\,r) = Der\,c\,(L(r))$ (I)
+\end{tabular}
+\end{center}
+
+We have $der\,c\,(r^*) = der\,c\,r\cdot r^*$. Which means $L(der\,c\,(r^*)) = L(der\,c\,r\cdot r^*)$ and
+further $L(der\,c\,r) \,@\, L(r^*)$. By induction hypothesis (I) we know that is equal to 
+$(Der\,c\,L(r)) \,@\, L(r^*)$. (*)
+
 \end{itemize}
 
+
+
+
+Let us now analyse $Der\,c\,L(r^*)$, which is equal to $Der\,c\,((L(r))^*)$. Now $(L(r))^*$ is defined
+as $\bigcup_{n \ge 0} L(r)$. We can write this as $L(r)^0 \cup \bigcup_{n \ge 1} L(r)$, where we just 
+separated the first union and then let the ``big-union'' start from $1$. Form this we can already infer
+
+\begin{center}
+$Der\,c\,(L(r^*)) = Der\,c\,(L(r)^0 \cup \bigcup_{n \ge 1} L(r)) = (Der\,c\,L(r)^0) \cup Der\,c\,(\bigcup_{n \ge 1} L(r))$
+\end{center}
+
+The first union ``disappears'' since $Der\,c\,(L(r)^0) = \varnothing$.
+
+
 \end{document}
 
 %%% Local Variables: