Metamath Proof Explorer

Theorem swrdccatin1

Description: The subword of a concatenation of two words within the first of the concatenated words. (Contributed by Alexander van der Vekens, 28-Mar-2018)

Ref Expression
Assertion swrdccatin1 
|- ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( A substr <. M , N >. ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( ( # ` A ) = 0 -> ( 0 ... ( # ` A ) ) = ( 0 ... 0 ) )
2 1 eleq2d 
 |-  ( ( # ` A ) = 0 -> ( N e. ( 0 ... ( # ` A ) ) <-> N e. ( 0 ... 0 ) ) )
3 elfz1eq 
 |-  ( N e. ( 0 ... 0 ) -> N = 0 )
4 elfz1eq 
 |-  ( M e. ( 0 ... 0 ) -> M = 0 )
5 swrd00 
 |-  ( ( A ++ B ) substr <. 0 , 0 >. ) = (/)
6 swrd00 
 |-  ( A substr <. 0 , 0 >. ) = (/)
7 5 6 eqtr4i 
 |-  ( ( A ++ B ) substr <. 0 , 0 >. ) = ( A substr <. 0 , 0 >. )
8 opeq1 
 |-  ( M = 0 -> <. M , 0 >. = <. 0 , 0 >. )
9 8 oveq2d 
 |-  ( M = 0 -> ( ( A ++ B ) substr <. M , 0 >. ) = ( ( A ++ B ) substr <. 0 , 0 >. ) )
10 8 oveq2d 
 |-  ( M = 0 -> ( A substr <. M , 0 >. ) = ( A substr <. 0 , 0 >. ) )
11 7 9 10 3eqtr4a 
 |-  ( M = 0 -> ( ( A ++ B ) substr <. M , 0 >. ) = ( A substr <. M , 0 >. ) )
12 4 11 syl 
 |-  ( M e. ( 0 ... 0 ) -> ( ( A ++ B ) substr <. M , 0 >. ) = ( A substr <. M , 0 >. ) )
13 oveq2 
 |-  ( N = 0 -> ( 0 ... N ) = ( 0 ... 0 ) )
14 13 eleq2d 
 |-  ( N = 0 -> ( M e. ( 0 ... N ) <-> M e. ( 0 ... 0 ) ) )
15 opeq2 
 |-  ( N = 0 -> <. M , N >. = <. M , 0 >. )
16 15 oveq2d 
 |-  ( N = 0 -> ( ( A ++ B ) substr <. M , N >. ) = ( ( A ++ B ) substr <. M , 0 >. ) )
17 15 oveq2d 
 |-  ( N = 0 -> ( A substr <. M , N >. ) = ( A substr <. M , 0 >. ) )
18 16 17 eqeq12d 
 |-  ( N = 0 -> ( ( ( A ++ B ) substr <. M , N >. ) = ( A substr <. M , N >. ) <-> ( ( A ++ B ) substr <. M , 0 >. ) = ( A substr <. M , 0 >. ) ) )
19 14 18 imbi12d 
 |-  ( N = 0 -> ( ( M e. ( 0 ... N ) -> ( ( A ++ B ) substr <. M , N >. ) = ( A substr <. M , N >. ) ) <-> ( M e. ( 0 ... 0 ) -> ( ( A ++ B ) substr <. M , 0 >. ) = ( A substr <. M , 0 >. ) ) ) )
20 12 19 mpbiri 
 |-  ( N = 0 -> ( M e. ( 0 ... N ) -> ( ( A ++ B ) substr <. M , N >. ) = ( A substr <. M , N >. ) ) )
21 3 20 syl 
 |-  ( N e. ( 0 ... 0 ) -> ( M e. ( 0 ... N ) -> ( ( A ++ B ) substr <. M , N >. ) = ( A substr <. M , N >. ) ) )
22 2 21 syl6bi 
 |-  ( ( # ` A ) = 0 -> ( N e. ( 0 ... ( # ` A ) ) -> ( M e. ( 0 ... N ) -> ( ( A ++ B ) substr <. M , N >. ) = ( A substr <. M , N >. ) ) ) )
23 22 impcomd 
 |-  ( ( # ` A ) = 0 -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( A substr <. M , N >. ) ) )
24 23 adantl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) = 0 ) -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( A substr <. M , N >. ) ) )
25 ccatcl 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( A ++ B ) e. Word V )
26 25 ad2antrr 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) =/= 0 ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) ) -> ( A ++ B ) e. Word V )
27 simprl 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) =/= 0 ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) ) -> M e. ( 0 ... N ) )
28 elfzelfzccat 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( N e. ( 0 ... ( # ` A ) ) -> N e. ( 0 ... ( # ` ( A ++ B ) ) ) ) )
29 28 imp 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ N e. ( 0 ... ( # ` A ) ) ) -> N e. ( 0 ... ( # ` ( A ++ B ) ) ) )
30 29 ad2ant2rl 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) =/= 0 ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) ) -> N e. ( 0 ... ( # ` ( A ++ B ) ) ) )
31 swrdvalfn 
 |-  ( ( ( A ++ B ) e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` ( A ++ B ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) Fn ( 0 ..^ ( N - M ) ) )
32 26 27 30 31 syl3anc 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) =/= 0 ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) Fn ( 0 ..^ ( N - M ) ) )
33 3anass 
 |-  ( ( A e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) <-> ( A e. Word V /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) ) )
34 33 simplbi2 
 |-  ( A e. Word V -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) -> ( A e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) ) )
35 34 ad2antrr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) =/= 0 ) -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) -> ( A e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) ) )
36 35 imp 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) =/= 0 ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) ) -> ( A e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) )
37 swrdvalfn 
 |-  ( ( A e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) -> ( A substr <. M , N >. ) Fn ( 0 ..^ ( N - M ) ) )
38 36 37 syl 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) =/= 0 ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) ) -> ( A substr <. M , N >. ) Fn ( 0 ..^ ( N - M ) ) )
39 simp-4l 
 |-  ( ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) =/= 0 ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) -> A e. Word V )
40 simp-4r 
 |-  ( ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) =/= 0 ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) -> B e. Word V )
41 elfznn0 
 |-  ( M e. ( 0 ... N ) -> M e. NN0 )
42 nn0addcl 
 |-  ( ( k e. NN0 /\ M e. NN0 ) -> ( k + M ) e. NN0 )
43 42 expcom 
 |-  ( M e. NN0 -> ( k e. NN0 -> ( k + M ) e. NN0 ) )
44 41 43 syl 
 |-  ( M e. ( 0 ... N ) -> ( k e. NN0 -> ( k + M ) e. NN0 ) )
45 44 ad2antrl 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) =/= 0 ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) ) -> ( k e. NN0 -> ( k + M ) e. NN0 ) )
46 elfzonn0 
 |-  ( k e. ( 0 ..^ ( N - M ) ) -> k e. NN0 )
47 45 46 impel 
 |-  ( ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) =/= 0 ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) -> ( k + M ) e. NN0 )
48 lencl 
 |-  ( A e. Word V -> ( # ` A ) e. NN0 )
49 elnnne0 
 |-  ( ( # ` A ) e. NN <-> ( ( # ` A ) e. NN0 /\ ( # ` A ) =/= 0 ) )
50 49 simplbi2 
 |-  ( ( # ` A ) e. NN0 -> ( ( # ` A ) =/= 0 -> ( # ` A ) e. NN ) )
51 48 50 syl 
 |-  ( A e. Word V -> ( ( # ` A ) =/= 0 -> ( # ` A ) e. NN ) )
52 51 adantr 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( # ` A ) =/= 0 -> ( # ` A ) e. NN ) )
53 52 imp 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) =/= 0 ) -> ( # ` A ) e. NN )
54 53 ad2antrr 
 |-  ( ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) =/= 0 ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) -> ( # ` A ) e. NN )
55 elfzo0 
 |-  ( k e. ( 0 ..^ ( N - M ) ) <-> ( k e. NN0 /\ ( N - M ) e. NN /\ k < ( N - M ) ) )
56 elfz2nn0 
 |-  ( N e. ( 0 ... ( # ` A ) ) <-> ( N e. NN0 /\ ( # ` A ) e. NN0 /\ N <_ ( # ` A ) ) )
57 nn0re 
 |-  ( k e. NN0 -> k e. RR )
58 57 ad2antrl 
 |-  ( ( ( N e. NN0 /\ ( # ` A ) e. NN0 ) /\ ( k e. NN0 /\ M e. NN0 ) ) -> k e. RR )
59 nn0re 
 |-  ( M e. NN0 -> M e. RR )
60 59 ad2antll 
 |-  ( ( ( N e. NN0 /\ ( # ` A ) e. NN0 ) /\ ( k e. NN0 /\ M e. NN0 ) ) -> M e. RR )
61 nn0re 
 |-  ( N e. NN0 -> N e. RR )
62 61 ad2antrr 
 |-  ( ( ( N e. NN0 /\ ( # ` A ) e. NN0 ) /\ ( k e. NN0 /\ M e. NN0 ) ) -> N e. RR )
63 58 60 62 ltaddsubd 
 |-  ( ( ( N e. NN0 /\ ( # ` A ) e. NN0 ) /\ ( k e. NN0 /\ M e. NN0 ) ) -> ( ( k + M ) < N <-> k < ( N - M ) ) )
64 nn0readdcl 
 |-  ( ( k e. NN0 /\ M e. NN0 ) -> ( k + M ) e. RR )
65 64 adantl 
 |-  ( ( ( N e. NN0 /\ ( # ` A ) e. NN0 ) /\ ( k e. NN0 /\ M e. NN0 ) ) -> ( k + M ) e. RR )
66 nn0re 
 |-  ( ( # ` A ) e. NN0 -> ( # ` A ) e. RR )
67 66 ad2antlr 
 |-  ( ( ( N e. NN0 /\ ( # ` A ) e. NN0 ) /\ ( k e. NN0 /\ M e. NN0 ) ) -> ( # ` A ) e. RR )
68 ltletr 
 |-  ( ( ( k + M ) e. RR /\ N e. RR /\ ( # ` A ) e. RR ) -> ( ( ( k + M ) < N /\ N <_ ( # ` A ) ) -> ( k + M ) < ( # ` A ) ) )
69 65 62 67 68 syl3anc 
 |-  ( ( ( N e. NN0 /\ ( # ` A ) e. NN0 ) /\ ( k e. NN0 /\ M e. NN0 ) ) -> ( ( ( k + M ) < N /\ N <_ ( # ` A ) ) -> ( k + M ) < ( # ` A ) ) )
70 69 expd 
 |-  ( ( ( N e. NN0 /\ ( # ` A ) e. NN0 ) /\ ( k e. NN0 /\ M e. NN0 ) ) -> ( ( k + M ) < N -> ( N <_ ( # ` A ) -> ( k + M ) < ( # ` A ) ) ) )
71 63 70 sylbird 
 |-  ( ( ( N e. NN0 /\ ( # ` A ) e. NN0 ) /\ ( k e. NN0 /\ M e. NN0 ) ) -> ( k < ( N - M ) -> ( N <_ ( # ` A ) -> ( k + M ) < ( # ` A ) ) ) )
72 71 ex 
 |-  ( ( N e. NN0 /\ ( # ` A ) e. NN0 ) -> ( ( k e. NN0 /\ M e. NN0 ) -> ( k < ( N - M ) -> ( N <_ ( # ` A ) -> ( k + M ) < ( # ` A ) ) ) ) )
73 72 com24 
 |-  ( ( N e. NN0 /\ ( # ` A ) e. NN0 ) -> ( N <_ ( # ` A ) -> ( k < ( N - M ) -> ( ( k e. NN0 /\ M e. NN0 ) -> ( k + M ) < ( # ` A ) ) ) ) )
74 73 3impia 
 |-  ( ( N e. NN0 /\ ( # ` A ) e. NN0 /\ N <_ ( # ` A ) ) -> ( k < ( N - M ) -> ( ( k e. NN0 /\ M e. NN0 ) -> ( k + M ) < ( # ` A ) ) ) )
75 74 com13 
 |-  ( ( k e. NN0 /\ M e. NN0 ) -> ( k < ( N - M ) -> ( ( N e. NN0 /\ ( # ` A ) e. NN0 /\ N <_ ( # ` A ) ) -> ( k + M ) < ( # ` A ) ) ) )
76 75 impancom 
 |-  ( ( k e. NN0 /\ k < ( N - M ) ) -> ( M e. NN0 -> ( ( N e. NN0 /\ ( # ` A ) e. NN0 /\ N <_ ( # ` A ) ) -> ( k + M ) < ( # ` A ) ) ) )
77 76 3adant2 
 |-  ( ( k e. NN0 /\ ( N - M ) e. NN /\ k < ( N - M ) ) -> ( M e. NN0 -> ( ( N e. NN0 /\ ( # ` A ) e. NN0 /\ N <_ ( # ` A ) ) -> ( k + M ) < ( # ` A ) ) ) )
78 77 com13 
 |-  ( ( N e. NN0 /\ ( # ` A ) e. NN0 /\ N <_ ( # ` A ) ) -> ( M e. NN0 -> ( ( k e. NN0 /\ ( N - M ) e. NN /\ k < ( N - M ) ) -> ( k + M ) < ( # ` A ) ) ) )
79 56 78 sylbi 
 |-  ( N e. ( 0 ... ( # ` A ) ) -> ( M e. NN0 -> ( ( k e. NN0 /\ ( N - M ) e. NN /\ k < ( N - M ) ) -> ( k + M ) < ( # ` A ) ) ) )
80 41 79 mpan9 
 |-  ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) -> ( ( k e. NN0 /\ ( N - M ) e. NN /\ k < ( N - M ) ) -> ( k + M ) < ( # ` A ) ) )
81 80 adantl 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) =/= 0 ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) ) -> ( ( k e. NN0 /\ ( N - M ) e. NN /\ k < ( N - M ) ) -> ( k + M ) < ( # ` A ) ) )
82 55 81 syl5bi 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) =/= 0 ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) ) -> ( k e. ( 0 ..^ ( N - M ) ) -> ( k + M ) < ( # ` A ) ) )
83 82 imp 
 |-  ( ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) =/= 0 ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) -> ( k + M ) < ( # ` A ) )
84 elfzo0 
 |-  ( ( k + M ) e. ( 0 ..^ ( # ` A ) ) <-> ( ( k + M ) e. NN0 /\ ( # ` A ) e. NN /\ ( k + M ) < ( # ` A ) ) )
85 47 54 83 84 syl3anbrc 
 |-  ( ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) =/= 0 ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) -> ( k + M ) e. ( 0 ..^ ( # ` A ) ) )
86 ccatval1 
 |-  ( ( A e. Word V /\ B e. Word V /\ ( k + M ) e. ( 0 ..^ ( # ` A ) ) ) -> ( ( A ++ B ) ` ( k + M ) ) = ( A ` ( k + M ) ) )
87 39 40 85 86 syl3anc 
 |-  ( ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) =/= 0 ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) -> ( ( A ++ B ) ` ( k + M ) ) = ( A ` ( k + M ) ) )
88 25 ad5ant12 
 |-  ( ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) =/= 0 ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) -> ( A ++ B ) e. Word V )
89 simplrl 
 |-  ( ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) =/= 0 ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) -> M e. ( 0 ... N ) )
90 30 adantr 
 |-  ( ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) =/= 0 ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) -> N e. ( 0 ... ( # ` ( A ++ B ) ) ) )
91 simpr 
 |-  ( ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) =/= 0 ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) -> k e. ( 0 ..^ ( N - M ) ) )
92 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 ) ) )
93 88 89 90 91 92 syl31anc 
 |-  ( ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) =/= 0 ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` k ) = ( ( A ++ B ) ` ( k + M ) ) )
94 swrdfv 
 |-  ( ( ( A e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) -> ( ( A substr <. M , N >. ) ` k ) = ( A ` ( k + M ) ) )
95 36 94 sylan 
 |-  ( ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) =/= 0 ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) -> ( ( A substr <. M , N >. ) ` k ) = ( A ` ( k + M ) ) )
96 87 93 95 3eqtr4d 
 |-  ( ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) =/= 0 ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` k ) = ( ( A substr <. M , N >. ) ` k ) )
97 32 38 96 eqfnfvd 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) =/= 0 ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( A substr <. M , N >. ) )
98 97 ex 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` A ) =/= 0 ) -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( A substr <. M , N >. ) ) )
99 24 98 pm2.61dane 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( A substr <. M , N >. ) ) )