Description: The range of a subword of a word is a subset of the set of symbols for the word. (Contributed by AV, 13-Nov-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | swrdrn | |- ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ran ( W substr <. M , N >. ) C_ V ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | swrdf | |- ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ( W substr <. M , N >. ) : ( 0 ..^ ( N - M ) ) --> V ) |
|
2 | 1 | frnd | |- ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ran ( W substr <. M , N >. ) C_ V ) |