Theorem pfxfn

Description: Value of the prefix extractor as function with domain. (Contributed by AV, 2-May-2020)

	Ref	Expression
Assertion	pfxfn	$$⊢\left(S\in \mathrm{Word}V\wedge L\in \left(0\dots \left|S\right|\right)\right)\to \left(S\mathrm{prefix}L\right)Fn\left(0..^L\right)$$

Proof

Step	Hyp	Ref	Expression
1		pfxf	$$⊢\left(S\in \mathrm{Word}V\wedge L\in \left(0\dots \left|S\right|\right)\right)\to \left(S\mathrm{prefix}L\right):\left(0..^L\right)⟶V$$
2	1	ffnd	$$⊢\left(S\in \mathrm{Word}V\wedge L\in \left(0\dots \left|S\right|\right)\right)\to \left(S\mathrm{prefix}L\right)Fn\left(0..^L\right)$$