\begin{definition}[Definition:Sequence/Empty Sequence]
An '''empty sequence''' is a (finite) sequence containing no terms.
Thus an '''empty sequence''' is a mapping from $\O$ to $S$, that is, the empty mapping.
Thus by definition an '''empty sequence''' is a (finite) sequence whose length is $0$.
\end{definition}