Theorem iswrdb

Description: A word over an alphabet is a function from an open range of nonnegative integers (of length equal to the length of the word) into the alphabet. (Contributed by Alexander van der Vekens, 30-Jul-2018)

	Ref	Expression
Assertion	iswrdb	$$⊢W\in \mathrm{Word}S\leftrightarrow W:\left(0..^\left|W\right|\right)⟶S$$

Proof

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