Theorem pfxrn

Description: The range of a prefix of a word is a subset of the set of symbols for the word. (Contributed by AV, 2-May-2020)

	Ref	Expression
Assertion	pfxrn	|- ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ran ( W prefix L ) C_ V )

Proof

Step	Hyp	Ref	Expression
1		pfxf	|- ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( W prefix L ) : ( 0 ..^ L ) --> V )
2	1	frnd	|- ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ran ( W prefix L ) C_ V )