Definition df-word

Description: Define the class ofwords over a set. A word (sometimes also called a string) is a finite sequence of symbols from a set (alphabet) S . Definition in Section 9.1 of AhoHopUll p. 318. The domain is forced to be an initial segment of NN0 so that two words with the same symbols in the same order be equal. The set Word S is sometimes denoted by S*, using the Kleene star, although the Kleene star, or Kleene closure, is sometimes reserved to denote an operation on languages. The set Word S equipped with concatenation is the free monoid over S , and the monoid unit is the empty word (see frmdval ). (Contributed by FL, 14-Jan-2014) (Revised by Stefan O'Rear, 14-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016)

	Ref	Expression
Assertion	df-word	⊢ Word 𝑆 = { 𝑤 ∣ ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cS	⊢ 𝑆
1	0	cword	⊢ Word 𝑆
2		vw	⊢ 𝑤
3		vl	⊢ 𝑙
4		cn0	⊢ ℕ0
5	2	cv	⊢ 𝑤
6		cc0	⊢ 0
7		cfzo	⊢ ..^
8	3	cv	⊢ 𝑙
9	6 8 7	co	⊢ ( 0 ..^ 𝑙 )
10	9 0 5	wf	⊢ 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆
11	10 3 4	wrex	⊢ ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆
12	11 2	cab	⊢ { 𝑤 ∣ ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 }
13	1 12	wceq	⊢ Word 𝑆 = { 𝑤 ∣ ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 }