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 e. Word S -> dom W = ( 0 ..^ ( # ` W ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wrdf | |- ( W e. Word S -> W : ( 0 ..^ ( # ` W ) ) --> S ) |
|
| 2 | 1 | fdmd | |- ( W e. Word S -> dom W = ( 0 ..^ ( # ` W ) ) ) |