Description: Value of the prefix extractor as function with domain. (Contributed by AV, 2-May-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | pfxfn | |- ( ( S e. Word V /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S prefix L ) Fn ( 0 ..^ L ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pfxf | |- ( ( S e. Word V /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S prefix L ) : ( 0 ..^ L ) --> V ) |
|
2 | 1 | ffnd | |- ( ( S e. Word V /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S prefix L ) Fn ( 0 ..^ L ) ) |