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	⊢ ( 𝑊 ∈ Word 𝑆 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		wrdfin	⊢ ( 𝑊 ∈ Word 𝑆 → 𝑊 ∈ Fin )
2		hashcl	⊢ ( 𝑊 ∈ Fin → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
3	1 2	syl	⊢ ( 𝑊 ∈ Word 𝑆 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )