Theorem sseqp1

Description: Value of the strong sequence builder function at a successor. (Contributed by Thierry Arnoux, 24-Apr-2019)

	Ref	Expression
Hypotheses	sseqval.1	$$⊢\phi \to S\in \mathrm{V}$$
	sseqval.2	$$⊢\phi \to M\in \mathrm{Word}S$$
	sseqval.3	$$⊢W=\mathrm{Word}S\cap {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge \left|M\right|}\right]$$
	sseqval.4	$$⊢\phi \to F:W⟶S$$
	sseqfv2.4	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge \left|M\right|}$$
Assertion	sseqp1	$$⊢\phi \to \left(M{\mathrm{seq}}_{str}F\right)\left(N\right)=F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right)$$

Proof

Step	Hyp	Ref	Expression
1		sseqval.1	$$⊢\phi \to S\in \mathrm{V}$$
2		sseqval.2	$$⊢\phi \to M\in \mathrm{Word}S$$
3		sseqval.3	$$⊢W=\mathrm{Word}S\cap {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge \left|M\right|}\right]$$
4		sseqval.4	$$⊢\phi \to F:W⟶S$$
5		sseqfv2.4	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge \left|M\right|}$$
6	1 2 3 4 5	sseqfv2	$$⊢\phi \to \left(M{\mathrm{seq}}_{str}F\right)\left(N\right)=\mathrm{lastS}\left(seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(N\right)\right)$$
7		fveq2	$$⊢i=\left|M\right|\to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(i\right)=seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(\left|M\right|\right)$$
8		oveq2	$$⊢i=\left|M\right|\to \left(0..^i\right)=\left(0..^\left|M\right|\right)$$
9	8	reseq2d	$$⊢i=\left|M\right|\to {\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}={\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^\left|M\right|\right)}$$
10	9	fveq2d	$$⊢i=\left|M\right|\to F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)=F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^\left|M\right|\right)}\right)$$
11	10	s1eqd	$$⊢i=\left|M\right|\to ⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)”⟩=⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^\left|M\right|\right)}\right)”⟩$$
12	9 11	oveq12d	$$⊢i=\left|M\right|\to \left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)”⟩=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^\left|M\right|\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^\left|M\right|\right)}\right)”⟩$$
13	7 12	eqeq12d	$$⊢i=\left|M\right|\to \left(seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(i\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)”⟩\leftrightarrow seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(\left|M\right|\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^\left|M\right|\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^\left|M\right|\right)}\right)”⟩\right)$$
14	13	imbi2d	$$⊢i=\left|M\right|\to \left(\left(\phi \to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(i\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)”⟩\right)\leftrightarrow \left(\phi \to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(\left|M\right|\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^\left|M\right|\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^\left|M\right|\right)}\right)”⟩\right)\right)$$
15		fveq2	$$⊢i=n\to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(i\right)=seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)$$
16		oveq2	$$⊢i=n\to \left(0..^i\right)=\left(0..^n\right)$$
17	16	reseq2d	$$⊢i=n\to {\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}={\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}$$
18	17	fveq2d	$$⊢i=n\to F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)=F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)$$
19	18	s1eqd	$$⊢i=n\to ⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)”⟩=⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩$$
20	17 19	oveq12d	$$⊢i=n\to \left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)”⟩=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩$$
21	15 20	eqeq12d	$$⊢i=n\to \left(seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(i\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)”⟩\leftrightarrow seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩\right)$$
22	21	imbi2d	$$⊢i=n\to \left(\left(\phi \to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(i\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)”⟩\right)\leftrightarrow \left(\phi \to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩\right)\right)$$
23		fveq2	$$⊢i=n+1\to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(i\right)=seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n+1\right)$$
24		oveq2	$$⊢i=n+1\to \left(0..^i\right)=\left(0..^n+1\right)$$
25	24	reseq2d	$$⊢i=n+1\to {\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}={\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n+1\right)}$$
26	25	fveq2d	$$⊢i=n+1\to F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)=F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n+1\right)}\right)$$
27	26	s1eqd	$$⊢i=n+1\to ⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)”⟩=⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n+1\right)}\right)”⟩$$
28	25 27	oveq12d	$$⊢i=n+1\to \left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)”⟩=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n+1\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n+1\right)}\right)”⟩$$
29	23 28	eqeq12d	$$⊢i=n+1\to \left(seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(i\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)”⟩\leftrightarrow seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n+1\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n+1\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n+1\right)}\right)”⟩\right)$$
30	29	imbi2d	$$⊢i=n+1\to \left(\left(\phi \to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(i\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)”⟩\right)\leftrightarrow \left(\phi \to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n+1\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n+1\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n+1\right)}\right)”⟩\right)\right)$$
31		fveq2	$$⊢i=N\to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(i\right)=seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(N\right)$$
32		oveq2	$$⊢i=N\to \left(0..^i\right)=\left(0..^N\right)$$
33	32	reseq2d	$$⊢i=N\to {\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}={\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}$$
34	33	fveq2d	$$⊢i=N\to F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)=F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right)$$
35	34	s1eqd	$$⊢i=N\to ⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)”⟩=⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right)”⟩$$
36	33 35	oveq12d	$$⊢i=N\to \left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)”⟩=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right)”⟩$$
37	31 36	eqeq12d	$$⊢i=N\to \left(seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(i\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)”⟩\leftrightarrow seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(N\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right)”⟩\right)$$
38	37	imbi2d	$$⊢i=N\to \left(\left(\phi \to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(i\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^i\right)}\right)”⟩\right)\leftrightarrow \left(\phi \to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(N\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right)”⟩\right)\right)$$
39		ovex	$$⊢M\mathrm{++}⟨“F\left(M\right)”⟩\in \mathrm{V}$$
40		lencl	$$⊢M\in \mathrm{Word}S\to \left|M\right|\in {\mathbb{N}}_0$$
41	2 40	syl	$$⊢\phi \to \left|M\right|\in {\mathbb{N}}_0$$
42		fvconst2g	$$⊢\left(M\mathrm{++}⟨“F\left(M\right)”⟩\in \mathrm{V}\wedge \left|M\right|\in {\mathbb{N}}_0\right)\to \left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\left(\left|M\right|\right)=M\mathrm{++}⟨“F\left(M\right)”⟩$$
43	39 41 42	sylancr	$$⊢\phi \to \left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\left(\left|M\right|\right)=M\mathrm{++}⟨“F\left(M\right)”⟩$$
44	40	nn0zd	$$⊢M\in \mathrm{Word}S\to \left|M\right|\in \mathbb{Z}$$
45		seq1	$$⊢\left|M\right|\in \mathbb{Z}\to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(\left|M\right|\right)=\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\left(\left|M\right|\right)$$
46	2 44 45	3syl	$$⊢\phi \to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(\left|M\right|\right)=\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\left(\left|M\right|\right)$$
47	1 2 3 4	sseqfres	$$⊢\phi \to {\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^\left|M\right|\right)}=M$$
48	47	fveq2d	$$⊢\phi \to F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^\left|M\right|\right)}\right)=F\left(M\right)$$
49	48	s1eqd	$$⊢\phi \to ⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^\left|M\right|\right)}\right)”⟩=⟨“F\left(M\right)”⟩$$
50	47 49	oveq12d	$$⊢\phi \to \left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^\left|M\right|\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^\left|M\right|\right)}\right)”⟩=M\mathrm{++}⟨“F\left(M\right)”⟩$$
51	43 46 50	3eqtr4d	$$⊢\phi \to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(\left|M\right|\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^\left|M\right|\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^\left|M\right|\right)}\right)”⟩$$
52	51	a1i	$$⊢\left|M\right|\in \mathbb{Z}\to \left(\phi \to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(\left|M\right|\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^\left|M\right|\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^\left|M\right|\right)}\right)”⟩\right)$$
53		seqp1	$$⊢n\in {\mathbb{Z}}_{\ge \left|M\right|}\to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n+1\right)=seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right)\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\left(n+1\right)$$
54	53	adantl	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n+1\right)=seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right)\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\left(n+1\right)$$
55		id	$$⊢x=a\to x=a$$
56		fveq2	$$⊢x=a\to F\left(x\right)=F\left(a\right)$$
57	56	s1eqd	$$⊢x=a\to ⟨“F\left(x\right)”⟩=⟨“F\left(a\right)”⟩$$
58	55 57	oveq12d	$$⊢x=a\to x\mathrm{++}⟨“F\left(x\right)”⟩=a\mathrm{++}⟨“F\left(a\right)”⟩$$
59		eqidd	$$⊢y=b\to a\mathrm{++}⟨“F\left(a\right)”⟩=a\mathrm{++}⟨“F\left(a\right)”⟩$$
60	58 59	cbvmpov	$$⊢\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right)=\left(a\in \mathrm{V},b\in \mathrm{V}⟼a\mathrm{++}⟨“F\left(a\right)”⟩\right)$$
61	60	a1i	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\to \left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right)=\left(a\in \mathrm{V},b\in \mathrm{V}⟼a\mathrm{++}⟨“F\left(a\right)”⟩\right)$$
62		simprl	$$⊢\left(\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\wedge \left(a=seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\wedge b=\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\left(n+1\right)\right)\right)\to a=seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)$$
63	62	fveq2d	$$⊢\left(\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\wedge \left(a=seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\wedge b=\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\left(n+1\right)\right)\right)\to F\left(a\right)=F\left(seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\right)$$
64	63	s1eqd	$$⊢\left(\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\wedge \left(a=seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\wedge b=\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\left(n+1\right)\right)\right)\to ⟨“F\left(a\right)”⟩=⟨“F\left(seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\right)”⟩$$
65	62 64	oveq12d	$$⊢\left(\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\wedge \left(a=seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\wedge b=\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\left(n+1\right)\right)\right)\to a\mathrm{++}⟨“F\left(a\right)”⟩=seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\mathrm{++}⟨“F\left(seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\right)”⟩$$
66		fvexd	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\in \mathrm{V}$$
67		fvexd	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\to \left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\left(n+1\right)\in \mathrm{V}$$
68		ovex	$$⊢seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\mathrm{++}⟨“F\left(seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\right)”⟩\in \mathrm{V}$$
69	68	a1i	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\mathrm{++}⟨“F\left(seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\right)”⟩\in \mathrm{V}$$
70	61 65 66 67 69	ovmpod	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right)\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\left(n+1\right)=seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\mathrm{++}⟨“F\left(seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\right)”⟩$$
71	54 70	eqtrd	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n+1\right)=seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\mathrm{++}⟨“F\left(seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\right)”⟩$$
72	71	adantr	$$⊢\left(\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\wedge seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩\right)\to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n+1\right)=seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\mathrm{++}⟨“F\left(seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\right)”⟩$$
73	1	adantr	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\to S\in \mathrm{V}$$
74	2	adantr	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\to M\in \mathrm{Word}S$$
75	4	adantr	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\to F:W⟶S$$
76		simpr	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\to n\in {\mathbb{Z}}_{\ge \left|M\right|}$$
77	73 74 3 75 76	sseqfv2	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\to \left(M{\mathrm{seq}}_{str}F\right)\left(n\right)=\mathrm{lastS}\left(seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\right)$$
78	77	adantr	$$⊢\left(\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\wedge seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩\right)\to \left(M{\mathrm{seq}}_{str}F\right)\left(n\right)=\mathrm{lastS}\left(seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\right)$$
79		simpr	$$⊢\left(\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\wedge seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩\right)\to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩$$
80	79	fveq2d	$$⊢\left(\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\wedge seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩\right)\to \mathrm{lastS}\left(seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\right)=\mathrm{lastS}\left(\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩\right)$$
81	1 2 3 4	sseqf	$$⊢\phi \to \left(M{\mathrm{seq}}_{str}F\right):{\mathbb{N}}_0⟶S$$
82		fzo0ssnn0	$$⊢\left(0..^n\right)\subseteq {\mathbb{N}}_0$$
83		fssres	$$⊢\left(\left(M{\mathrm{seq}}_{str}F\right):{\mathbb{N}}_0⟶S\wedge \left(0..^n\right)\subseteq {\mathbb{N}}_0\right)\to \left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right):\left(0..^n\right)⟶S$$
84	81 82 83	sylancl	$$⊢\phi \to \left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right):\left(0..^n\right)⟶S$$
85		iswrdi	$$⊢\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right):\left(0..^n\right)⟶S\to {\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\in \mathrm{Word}S$$
86	84 85	syl	$$⊢\phi \to {\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\in \mathrm{Word}S$$
87	86	adantr	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\to {\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\in \mathrm{Word}S$$
88		elex	$$⊢{\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\in \mathrm{Word}S\to {\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\in \mathrm{V}$$
89	87 88	syl	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\to {\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\in \mathrm{V}$$
90	81	adantr	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\to \left(M{\mathrm{seq}}_{str}F\right):{\mathbb{N}}_0⟶S$$
91		eluznn0	$$⊢\left(\left|M\right|\in {\mathbb{N}}_0\wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\to n\in {\mathbb{N}}_0$$
92	41 91	sylan	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\to n\in {\mathbb{N}}_0$$
93	73 90 92	subiwrdlen	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\to \left|{\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right|=n$$
94	93 76	eqeltrd	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\to \left|{\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right|\in {\mathbb{Z}}_{\ge \left|M\right|}$$
95		hashf	$$⊢\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}$$
96		ffn	$$⊢\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}\to \left|.\right|Fn\mathrm{V}$$
97		elpreima	$$⊢\left|.\right|Fn\mathrm{V}\to \left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\in {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge \left|M\right|}\right]\leftrightarrow \left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\in \mathrm{V}\wedge \left|{\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right|\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\right)$$
98	95 96 97	mp2b	$$⊢{\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\in {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge \left|M\right|}\right]\leftrightarrow \left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\in \mathrm{V}\wedge \left|{\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right|\in {\mathbb{Z}}_{\ge \left|M\right|}\right)$$
99	89 94 98	sylanbrc	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\to {\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\in {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge \left|M\right|}\right]$$
100	87 99	elind	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\to {\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\in \left(\mathrm{Word}S\cap {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge \left|M\right|}\right]\right)$$
101	100 3	eleqtrrdi	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\to {\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\in W$$
102	75 101	ffvelcdmd	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\to F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\in S$$
103		lswccats1	$$⊢\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\in \mathrm{Word}S\wedge F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\in S\right)\to \mathrm{lastS}\left(\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩\right)=F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)$$
104	87 102 103	syl2anc	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\to \mathrm{lastS}\left(\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩\right)=F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)$$
105	104	adantr	$$⊢\left(\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\wedge seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩\right)\to \mathrm{lastS}\left(\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩\right)=F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)$$
106	78 80 105	3eqtrrd	$$⊢\left(\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\wedge seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩\right)\to F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)=\left(M{\mathrm{seq}}_{str}F\right)\left(n\right)$$
107	106	s1eqd	$$⊢\left(\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\wedge seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩\right)\to ⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩=⟨“\left(M{\mathrm{seq}}_{str}F\right)\left(n\right)”⟩$$
108	107	oveq2d	$$⊢\left(\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\wedge seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩\right)\to \left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“\left(M{\mathrm{seq}}_{str}F\right)\left(n\right)”⟩$$
109	73 90 92	iwrdsplit	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\to {\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n+1\right)}=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“\left(M{\mathrm{seq}}_{str}F\right)\left(n\right)”⟩$$
110	109	adantr	$$⊢\left(\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\wedge seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩\right)\to {\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n+1\right)}=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“\left(M{\mathrm{seq}}_{str}F\right)\left(n\right)”⟩$$
111	108 79 110	3eqtr4d	$$⊢\left(\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\wedge seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩\right)\to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)={\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n+1\right)}$$
112	111	fveq2d	$$⊢\left(\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\wedge seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩\right)\to F\left(seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\right)=F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n+1\right)}\right)$$
113	112	s1eqd	$$⊢\left(\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\wedge seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩\right)\to ⟨“F\left(seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\right)”⟩=⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n+1\right)}\right)”⟩$$
114	111 113	oveq12d	$$⊢\left(\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\wedge seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩\right)\to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\mathrm{++}⟨“F\left(seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)\right)”⟩=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n+1\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n+1\right)}\right)”⟩$$
115	72 114	eqtrd	$$⊢\left(\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\wedge seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩\right)\to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n+1\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n+1\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n+1\right)}\right)”⟩$$
116	115	ex	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\to \left(seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩\to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n+1\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n+1\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n+1\right)}\right)”⟩\right)$$
117	116	expcom	$$⊢n\in {\mathbb{Z}}_{\ge \left|M\right|}\to \left(\phi \to \left(seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩\to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n+1\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n+1\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n+1\right)}\right)”⟩\right)\right)$$
118	117	a2d	$$⊢n\in {\mathbb{Z}}_{\ge \left|M\right|}\to \left(\left(\phi \to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n\right)}\right)”⟩\right)\to \left(\phi \to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(n+1\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n+1\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^n+1\right)}\right)”⟩\right)\right)$$
119	14 22 30 38 52 118	uzind4	$$⊢N\in {\mathbb{Z}}_{\ge \left|M\right|}\to \left(\phi \to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(N\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right)”⟩\right)$$
120	5 119	mpcom	$$⊢\phi \to seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(N\right)=\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right)”⟩$$
121	120	fveq2d	$$⊢\phi \to \mathrm{lastS}\left(seq\left|M\right|\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\mathrm{++}⟨“F\left(x\right)”⟩\right),\left({\mathbb{N}}_0\times \left\{M\mathrm{++}⟨“F\left(M\right)”⟩\right\}\right)\right)\left(N\right)\right)=\mathrm{lastS}\left(\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right)”⟩\right)$$
122		fzo0ssnn0	$$⊢\left(0..^N\right)\subseteq {\mathbb{N}}_0$$
123		fssres	$$⊢\left(\left(M{\mathrm{seq}}_{str}F\right):{\mathbb{N}}_0⟶S\wedge \left(0..^N\right)\subseteq {\mathbb{N}}_0\right)\to \left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right):\left(0..^N\right)⟶S$$
124	81 122 123	sylancl	$$⊢\phi \to \left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right):\left(0..^N\right)⟶S$$
125		iswrdi	$$⊢\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right):\left(0..^N\right)⟶S\to {\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\in \mathrm{Word}S$$
126	124 125	syl	$$⊢\phi \to {\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\in \mathrm{Word}S$$
127		elex	$$⊢{\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\in \mathrm{Word}S\to {\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\in \mathrm{V}$$
128	126 127	syl	$$⊢\phi \to {\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\in \mathrm{V}$$
129		eluznn0	$$⊢\left(\left|M\right|\in {\mathbb{N}}_0\wedge N\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\to N\in {\mathbb{N}}_0$$
130	41 5 129	syl2anc	$$⊢\phi \to N\in {\mathbb{N}}_0$$
131	1 81 130	subiwrdlen	$$⊢\phi \to \left|{\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right|=N$$
132	131 5	eqeltrd	$$⊢\phi \to \left|{\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right|\in {\mathbb{Z}}_{\ge \left|M\right|}$$
133		elpreima	$$⊢\left|.\right|Fn\mathrm{V}\to \left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\in {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge \left|M\right|}\right]\leftrightarrow \left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\in \mathrm{V}\wedge \left|{\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right|\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\right)$$
134	95 96 133	mp2b	$$⊢{\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\in {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge \left|M\right|}\right]\leftrightarrow \left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\in \mathrm{V}\wedge \left|{\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right|\in {\mathbb{Z}}_{\ge \left|M\right|}\right)$$
135	128 132 134	sylanbrc	$$⊢\phi \to {\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\in {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge \left|M\right|}\right]$$
136	126 135	elind	$$⊢\phi \to {\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\in \left(\mathrm{Word}S\cap {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge \left|M\right|}\right]\right)$$
137	136 3	eleqtrrdi	$$⊢\phi \to {\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\in W$$
138	4 137	ffvelcdmd	$$⊢\phi \to F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right)\in S$$
139		lswccats1	$$⊢\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\in \mathrm{Word}S\wedge F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right)\in S\right)\to \mathrm{lastS}\left(\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right)”⟩\right)=F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right)$$
140	126 138 139	syl2anc	$$⊢\phi \to \mathrm{lastS}\left(\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right)\mathrm{++}⟨“F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right)”⟩\right)=F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right)$$
141	6 121 140	3eqtrd	$$⊢\phi \to \left(M{\mathrm{seq}}_{str}F\right)\left(N\right)=F\left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^N\right)}\right)$$