This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pfxccatin12lem3

Description: Lemma 3 for pfxccatin12 . (Contributed by AV, 30-Mar-2018) (Revised by AV, 27-May-2018)

Ref Expression
Hypothesis swrdccatin2.l 
|- L = ( # ` A )
Assertion pfxccatin12lem3 
|- ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( K e. ( 0 ..^ ( N - M ) ) /\ K e. ( 0 ..^ ( L - M ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` K ) = ( ( A substr <. M , L >. ) ` K ) ) )

Proof

Step Hyp Ref Expression
1 swrdccatin2.l 
 |-  L = ( # ` A )
2 simpll 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ K e. ( 0 ..^ ( L - M ) ) ) ) -> ( A e. Word V /\ B e. Word V ) )
3 elfzo0 
 |-  ( K e. ( 0 ..^ ( L - M ) ) <-> ( K e. NN0 /\ ( L - M ) e. NN /\ K < ( L - M ) ) )
4 lencl 
 |-  ( A e. Word V -> ( # ` A ) e. NN0 )
5 elfz2nn0 
 |-  ( M e. ( 0 ... L ) <-> ( M e. NN0 /\ L e. NN0 /\ M <_ L ) )
6 nn0addcl 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> ( K + M ) e. NN0 )
7 6 ex 
 |-  ( K e. NN0 -> ( M e. NN0 -> ( K + M ) e. NN0 ) )
8 7 3ad2ant1 
 |-  ( ( K e. NN0 /\ ( L - M ) e. NN /\ K < ( L - M ) ) -> ( M e. NN0 -> ( K + M ) e. NN0 ) )
9 8 com12 
 |-  ( M e. NN0 -> ( ( K e. NN0 /\ ( L - M ) e. NN /\ K < ( L - M ) ) -> ( K + M ) e. NN0 ) )
10 9 3ad2ant1 
 |-  ( ( M e. NN0 /\ L e. NN0 /\ M <_ L ) -> ( ( K e. NN0 /\ ( L - M ) e. NN /\ K < ( L - M ) ) -> ( K + M ) e. NN0 ) )
11 10 imp 
 |-  ( ( ( M e. NN0 /\ L e. NN0 /\ M <_ L ) /\ ( K e. NN0 /\ ( L - M ) e. NN /\ K < ( L - M ) ) ) -> ( K + M ) e. NN0 )
12 elnnz 
 |-  ( ( L - M ) e. NN <-> ( ( L - M ) e. ZZ /\ 0 < ( L - M ) ) )
13 nn0re 
 |-  ( M e. NN0 -> M e. RR )
14 nn0re 
 |-  ( L e. NN0 -> L e. RR )
15 posdif 
 |-  ( ( M e. RR /\ L e. RR ) -> ( M < L <-> 0 < ( L - M ) ) )
16 13 14 15 syl2an 
 |-  ( ( M e. NN0 /\ L e. NN0 ) -> ( M < L <-> 0 < ( L - M ) ) )
17 elnn0z 
 |-  ( M e. NN0 <-> ( M e. ZZ /\ 0 <_ M ) )
18 0re 
 |-  0 e. RR
19 zre 
 |-  ( M e. ZZ -> M e. RR )
20 lelttr 
 |-  ( ( 0 e. RR /\ M e. RR /\ L e. RR ) -> ( ( 0 <_ M /\ M < L ) -> 0 < L ) )
21 18 19 14 20 mp3an3an 
 |-  ( ( M e. ZZ /\ L e. NN0 ) -> ( ( 0 <_ M /\ M < L ) -> 0 < L ) )
22 nn0z 
 |-  ( L e. NN0 -> L e. ZZ )
23 22 anim1i 
 |-  ( ( L e. NN0 /\ 0 < L ) -> ( L e. ZZ /\ 0 < L ) )
24 elnnz 
 |-  ( L e. NN <-> ( L e. ZZ /\ 0 < L ) )
25 23 24 sylibr 
 |-  ( ( L e. NN0 /\ 0 < L ) -> L e. NN )
26 25 ex 
 |-  ( L e. NN0 -> ( 0 < L -> L e. NN ) )
27 26 adantl 
 |-  ( ( M e. ZZ /\ L e. NN0 ) -> ( 0 < L -> L e. NN ) )
28 21 27 syld 
 |-  ( ( M e. ZZ /\ L e. NN0 ) -> ( ( 0 <_ M /\ M < L ) -> L e. NN ) )
29 28 expd 
 |-  ( ( M e. ZZ /\ L e. NN0 ) -> ( 0 <_ M -> ( M < L -> L e. NN ) ) )
30 29 impancom 
 |-  ( ( M e. ZZ /\ 0 <_ M ) -> ( L e. NN0 -> ( M < L -> L e. NN ) ) )
31 17 30 sylbi 
 |-  ( M e. NN0 -> ( L e. NN0 -> ( M < L -> L e. NN ) ) )
32 31 imp 
 |-  ( ( M e. NN0 /\ L e. NN0 ) -> ( M < L -> L e. NN ) )
33 16 32 sylbird 
 |-  ( ( M e. NN0 /\ L e. NN0 ) -> ( 0 < ( L - M ) -> L e. NN ) )
34 33 com12 
 |-  ( 0 < ( L - M ) -> ( ( M e. NN0 /\ L e. NN0 ) -> L e. NN ) )
35 12 34 simplbiim 
 |-  ( ( L - M ) e. NN -> ( ( M e. NN0 /\ L e. NN0 ) -> L e. NN ) )
36 35 3ad2ant2 
 |-  ( ( K e. NN0 /\ ( L - M ) e. NN /\ K < ( L - M ) ) -> ( ( M e. NN0 /\ L e. NN0 ) -> L e. NN ) )
37 36 com12 
 |-  ( ( M e. NN0 /\ L e. NN0 ) -> ( ( K e. NN0 /\ ( L - M ) e. NN /\ K < ( L - M ) ) -> L e. NN ) )
38 37 3adant3 
 |-  ( ( M e. NN0 /\ L e. NN0 /\ M <_ L ) -> ( ( K e. NN0 /\ ( L - M ) e. NN /\ K < ( L - M ) ) -> L e. NN ) )
39 38 imp 
 |-  ( ( ( M e. NN0 /\ L e. NN0 /\ M <_ L ) /\ ( K e. NN0 /\ ( L - M ) e. NN /\ K < ( L - M ) ) ) -> L e. NN )
40 nn0re 
 |-  ( K e. NN0 -> K e. RR )
41 40 adantr 
 |-  ( ( K e. NN0 /\ ( M e. NN0 /\ L e. NN0 /\ M <_ L ) ) -> K e. RR )
42 13 3ad2ant1 
 |-  ( ( M e. NN0 /\ L e. NN0 /\ M <_ L ) -> M e. RR )
43 42 adantl 
 |-  ( ( K e. NN0 /\ ( M e. NN0 /\ L e. NN0 /\ M <_ L ) ) -> M e. RR )
44 14 3ad2ant2 
 |-  ( ( M e. NN0 /\ L e. NN0 /\ M <_ L ) -> L e. RR )
45 44 adantl 
 |-  ( ( K e. NN0 /\ ( M e. NN0 /\ L e. NN0 /\ M <_ L ) ) -> L e. RR )
46 41 43 45 ltaddsubd 
 |-  ( ( K e. NN0 /\ ( M e. NN0 /\ L e. NN0 /\ M <_ L ) ) -> ( ( K + M ) < L <-> K < ( L - M ) ) )
47 46 exbiri 
 |-  ( K e. NN0 -> ( ( M e. NN0 /\ L e. NN0 /\ M <_ L ) -> ( K < ( L - M ) -> ( K + M ) < L ) ) )
48 47 com23 
 |-  ( K e. NN0 -> ( K < ( L - M ) -> ( ( M e. NN0 /\ L e. NN0 /\ M <_ L ) -> ( K + M ) < L ) ) )
49 48 imp 
 |-  ( ( K e. NN0 /\ K < ( L - M ) ) -> ( ( M e. NN0 /\ L e. NN0 /\ M <_ L ) -> ( K + M ) < L ) )
50 49 3adant2 
 |-  ( ( K e. NN0 /\ ( L - M ) e. NN /\ K < ( L - M ) ) -> ( ( M e. NN0 /\ L e. NN0 /\ M <_ L ) -> ( K + M ) < L ) )
51 50 impcom 
 |-  ( ( ( M e. NN0 /\ L e. NN0 /\ M <_ L ) /\ ( K e. NN0 /\ ( L - M ) e. NN /\ K < ( L - M ) ) ) -> ( K + M ) < L )
52 11 39 51 3jca 
 |-  ( ( ( M e. NN0 /\ L e. NN0 /\ M <_ L ) /\ ( K e. NN0 /\ ( L - M ) e. NN /\ K < ( L - M ) ) ) -> ( ( K + M ) e. NN0 /\ L e. NN /\ ( K + M ) < L ) )
53 52 ex 
 |-  ( ( M e. NN0 /\ L e. NN0 /\ M <_ L ) -> ( ( K e. NN0 /\ ( L - M ) e. NN /\ K < ( L - M ) ) -> ( ( K + M ) e. NN0 /\ L e. NN /\ ( K + M ) < L ) ) )
54 53 a1d 
 |-  ( ( M e. NN0 /\ L e. NN0 /\ M <_ L ) -> ( N e. ( L ... ( L + ( # ` B ) ) ) -> ( ( K e. NN0 /\ ( L - M ) e. NN /\ K < ( L - M ) ) -> ( ( K + M ) e. NN0 /\ L e. NN /\ ( K + M ) < L ) ) ) )
55 5 54 sylbi 
 |-  ( M e. ( 0 ... L ) -> ( N e. ( L ... ( L + ( # ` B ) ) ) -> ( ( K e. NN0 /\ ( L - M ) e. NN /\ K < ( L - M ) ) -> ( ( K + M ) e. NN0 /\ L e. NN /\ ( K + M ) < L ) ) ) )
56 55 imp 
 |-  ( ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( ( K e. NN0 /\ ( L - M ) e. NN /\ K < ( L - M ) ) -> ( ( K + M ) e. NN0 /\ L e. NN /\ ( K + M ) < L ) ) )
57 56 2a1i 
 |-  ( ( # ` A ) = L -> ( L e. NN0 -> ( ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( ( K e. NN0 /\ ( L - M ) e. NN /\ K < ( L - M ) ) -> ( ( K + M ) e. NN0 /\ L e. NN /\ ( K + M ) < L ) ) ) ) )
58 eleq1 
 |-  ( ( # ` A ) = L -> ( ( # ` A ) e. NN0 <-> L e. NN0 ) )
59 eleq1 
 |-  ( ( # ` A ) = L -> ( ( # ` A ) e. NN <-> L e. NN ) )
60 breq2 
 |-  ( ( # ` A ) = L -> ( ( K + M ) < ( # ` A ) <-> ( K + M ) < L ) )
61 59 60 3anbi23d 
 |-  ( ( # ` A ) = L -> ( ( ( K + M ) e. NN0 /\ ( # ` A ) e. NN /\ ( K + M ) < ( # ` A ) ) <-> ( ( K + M ) e. NN0 /\ L e. NN /\ ( K + M ) < L ) ) )
62 61 imbi2d 
 |-  ( ( # ` A ) = L -> ( ( ( K e. NN0 /\ ( L - M ) e. NN /\ K < ( L - M ) ) -> ( ( K + M ) e. NN0 /\ ( # ` A ) e. NN /\ ( K + M ) < ( # ` A ) ) ) <-> ( ( K e. NN0 /\ ( L - M ) e. NN /\ K < ( L - M ) ) -> ( ( K + M ) e. NN0 /\ L e. NN /\ ( K + M ) < L ) ) ) )
63 62 imbi2d 
 |-  ( ( # ` A ) = L -> ( ( ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( ( K e. NN0 /\ ( L - M ) e. NN /\ K < ( L - M ) ) -> ( ( K + M ) e. NN0 /\ ( # ` A ) e. NN /\ ( K + M ) < ( # ` A ) ) ) ) <-> ( ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( ( K e. NN0 /\ ( L - M ) e. NN /\ K < ( L - M ) ) -> ( ( K + M ) e. NN0 /\ L e. NN /\ ( K + M ) < L ) ) ) ) )
64 57 58 63 3imtr4d 
 |-  ( ( # ` A ) = L -> ( ( # ` A ) e. NN0 -> ( ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( ( K e. NN0 /\ ( L - M ) e. NN /\ K < ( L - M ) ) -> ( ( K + M ) e. NN0 /\ ( # ` A ) e. NN /\ ( K + M ) < ( # ` A ) ) ) ) ) )
65 64 eqcoms 
 |-  ( L = ( # ` A ) -> ( ( # ` A ) e. NN0 -> ( ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( ( K e. NN0 /\ ( L - M ) e. NN /\ K < ( L - M ) ) -> ( ( K + M ) e. NN0 /\ ( # ` A ) e. NN /\ ( K + M ) < ( # ` A ) ) ) ) ) )
66 1 4 65 mpsyl 
 |-  ( A e. Word V -> ( ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( ( K e. NN0 /\ ( L - M ) e. NN /\ K < ( L - M ) ) -> ( ( K + M ) e. NN0 /\ ( # ` A ) e. NN /\ ( K + M ) < ( # ` A ) ) ) ) )
67 66 adantr 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( ( K e. NN0 /\ ( L - M ) e. NN /\ K < ( L - M ) ) -> ( ( K + M ) e. NN0 /\ ( # ` A ) e. NN /\ ( K + M ) < ( # ` A ) ) ) ) )
68 67 imp 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( K e. NN0 /\ ( L - M ) e. NN /\ K < ( L - M ) ) -> ( ( K + M ) e. NN0 /\ ( # ` A ) e. NN /\ ( K + M ) < ( # ` A ) ) ) )
69 68 com12 
 |-  ( ( K e. NN0 /\ ( L - M ) e. NN /\ K < ( L - M ) ) -> ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( K + M ) e. NN0 /\ ( # ` A ) e. NN /\ ( K + M ) < ( # ` A ) ) ) )
70 3 69 sylbi 
 |-  ( K e. ( 0 ..^ ( L - M ) ) -> ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( K + M ) e. NN0 /\ ( # ` A ) e. NN /\ ( K + M ) < ( # ` A ) ) ) )
71 70 adantl 
 |-  ( ( K e. ( 0 ..^ ( N - M ) ) /\ K e. ( 0 ..^ ( L - M ) ) ) -> ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( K + M ) e. NN0 /\ ( # ` A ) e. NN /\ ( K + M ) < ( # ` A ) ) ) )
72 71 impcom 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ K e. ( 0 ..^ ( L - M ) ) ) ) -> ( ( K + M ) e. NN0 /\ ( # ` A ) e. NN /\ ( K + M ) < ( # ` A ) ) )
73 elfzo0 
 |-  ( ( K + M ) e. ( 0 ..^ ( # ` A ) ) <-> ( ( K + M ) e. NN0 /\ ( # ` A ) e. NN /\ ( K + M ) < ( # ` A ) ) )
74 72 73 sylibr 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ K e. ( 0 ..^ ( L - M ) ) ) ) -> ( K + M ) e. ( 0 ..^ ( # ` A ) ) )
75 df-3an 
 |-  ( ( A e. Word V /\ B e. Word V /\ ( K + M ) e. ( 0 ..^ ( # ` A ) ) ) <-> ( ( A e. Word V /\ B e. Word V ) /\ ( K + M ) e. ( 0 ..^ ( # ` A ) ) ) )
76 2 74 75 sylanbrc 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ K e. ( 0 ..^ ( L - M ) ) ) ) -> ( A e. Word V /\ B e. Word V /\ ( K + M ) e. ( 0 ..^ ( # ` A ) ) ) )
77 ccatval1 
 |-  ( ( A e. Word V /\ B e. Word V /\ ( K + M ) e. ( 0 ..^ ( # ` A ) ) ) -> ( ( A ++ B ) ` ( K + M ) ) = ( A ` ( K + M ) ) )
78 76 77 syl 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ K e. ( 0 ..^ ( L - M ) ) ) ) -> ( ( A ++ B ) ` ( K + M ) ) = ( A ` ( K + M ) ) )
79 1 pfxccatin12lem2c 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( A ++ B ) e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` ( A ++ B ) ) ) ) )
80 simpl 
 |-  ( ( K e. ( 0 ..^ ( N - M ) ) /\ K e. ( 0 ..^ ( L - M ) ) ) -> K e. ( 0 ..^ ( N - M ) ) )
81 swrdfv 
 |-  ( ( ( ( A ++ B ) e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` ( A ++ B ) ) ) ) /\ K e. ( 0 ..^ ( N - M ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` K ) = ( ( A ++ B ) ` ( K + M ) ) )
82 79 80 81 syl2an 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ K e. ( 0 ..^ ( L - M ) ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` K ) = ( ( A ++ B ) ` ( K + M ) ) )
83 simplll 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ K e. ( 0 ..^ ( L - M ) ) ) ) -> A e. Word V )
84 simplrl 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ K e. ( 0 ..^ ( L - M ) ) ) ) -> M e. ( 0 ... L ) )
85 1 eleq1i 
 |-  ( L e. NN0 <-> ( # ` A ) e. NN0 )
86 elnn0uz 
 |-  ( L e. NN0 <-> L e. ( ZZ>= ` 0 ) )
87 eluzfz2 
 |-  ( L e. ( ZZ>= ` 0 ) -> L e. ( 0 ... L ) )
88 86 87 sylbi 
 |-  ( L e. NN0 -> L e. ( 0 ... L ) )
89 1 oveq2i 
 |-  ( 0 ... L ) = ( 0 ... ( # ` A ) )
90 88 89 eleqtrdi 
 |-  ( L e. NN0 -> L e. ( 0 ... ( # ` A ) ) )
91 85 90 sylbir 
 |-  ( ( # ` A ) e. NN0 -> L e. ( 0 ... ( # ` A ) ) )
92 4 91 syl 
 |-  ( A e. Word V -> L e. ( 0 ... ( # ` A ) ) )
93 92 ad3antrrr 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ K e. ( 0 ..^ ( L - M ) ) ) ) -> L e. ( 0 ... ( # ` A ) ) )
94 simprr 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ K e. ( 0 ..^ ( L - M ) ) ) ) -> K e. ( 0 ..^ ( L - M ) ) )
95 swrdfv 
 |-  ( ( ( A e. Word V /\ M e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` A ) ) ) /\ K e. ( 0 ..^ ( L - M ) ) ) -> ( ( A substr <. M , L >. ) ` K ) = ( A ` ( K + M ) ) )
96 83 84 93 94 95 syl31anc 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ K e. ( 0 ..^ ( L - M ) ) ) ) -> ( ( A substr <. M , L >. ) ` K ) = ( A ` ( K + M ) ) )
97 78 82 96 3eqtr4d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ K e. ( 0 ..^ ( L - M ) ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` K ) = ( ( A substr <. M , L >. ) ` K ) )
98 97 ex 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( K e. ( 0 ..^ ( N - M ) ) /\ K e. ( 0 ..^ ( L - M ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` K ) = ( ( A substr <. M , L >. ) ` K ) ) )