--- a/ChengsongTanPhdThesis/Chapters/Finite.tex	Mon Jul 04 12:27:13 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Finite.tex	Mon Jul 04 12:43:03 2022 +0100
@@ -1046,7 +1046,7 @@
 \end{proof}
 \noindent
 This closed form has a variant which can be more convenient in later proofs:
-\begin{corollary}
+\begin{corollary}{altsClosedForm1}
 	If $s \neq []$ then 
 	$\rderssimp \; (\sum \; rs) \; s = 
 	\rsimp{(\sum \; (\map \; \rderssimp{\_}{s} \; rs))}$.
@@ -1498,8 +1498,7 @@
 \end{proof}
 
 \noindent
-where in (1) the $\textit{Suffix}( r_1, s)$ are the all the suffixes of $s$ where $\rderssimp{ r_1}{s'}$ is nullable ($s'$ being a suffix of $s$).
-The reason why we could write the derivatives of a sequence this way is described in section 2.
+(1) is by the corollary \ref{seqEstimate1}
 The term (2) is used to control (1). 
 That is because one can obtain an overall
 smaller regex list