Theorem lencl

Description: The length of a word is a nonnegative integer. This corresponds to the definition in Section 9.1 of AhoHopUll p. 318. (Contributed by Stefan O'Rear, 27-Aug-2015)

	Ref	Expression
Assertion	lencl	$$⊢W\in \mathrm{Word}S\to \left|W\right|\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		wrdfin	$$⊢W\in \mathrm{Word}S\to W\in \mathrm{Fin}$$
2		hashcl	$$⊢W\in \mathrm{Fin}\to \left|W\right|\in {\mathbb{N}}_0$$
3	1 2	syl	$$⊢W\in \mathrm{Word}S\to \left|W\right|\in {\mathbb{N}}_0$$