Theorem wrddm

Description: The indices of a word (i.e. its domain regarded as function) are elements of an open range of nonnegative integers (of length equal to the length of the word). (Contributed by AV, 2-May-2020)

	Ref	Expression
Assertion	wrddm	$$⊢W\in \mathrm{Word}S\to \mathrm{dom}W=\left(0..^\left|W\right|\right)$$

Proof

Step	Hyp	Ref	Expression
1		wrdf	$$⊢W\in \mathrm{Word}S\to W:\left(0..^\left|W\right|\right)⟶S$$
2	1	fdmd	$$⊢W\in \mathrm{Word}S\to \mathrm{dom}W=\left(0..^\left|W\right|\right)$$