Step | Hyp | Ref
| Expression |
1 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑔 = ∅ → (𝐹 ++ 𝑔) = (𝐹 ++ ∅)) |
2 | 1 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑔 = ∅ → (𝑇‘(𝐹 ++ 𝑔)) = (𝑇‘(𝐹 ++ ∅))) |
3 | 2 | fveq1d 6105 |
. . . . . 6
⊢ (𝑔 = ∅ → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘(𝐹 ++ ∅))‘𝑁)) |
4 | 3 | eqeq1d 2612 |
. . . . 5
⊢ (𝑔 = ∅ → (((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁) ↔ ((𝑇‘(𝐹 ++ ∅))‘𝑁) = ((𝑇‘𝐹)‘𝑁))) |
5 | 4 | imbi2d 329 |
. . . 4
⊢ (𝑔 = ∅ → (((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) ↔ ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ ∅))‘𝑁) = ((𝑇‘𝐹)‘𝑁)))) |
6 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑔 = 𝑒 → (𝐹 ++ 𝑔) = (𝐹 ++ 𝑒)) |
7 | 6 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑔 = 𝑒 → (𝑇‘(𝐹 ++ 𝑔)) = (𝑇‘(𝐹 ++ 𝑒))) |
8 | 7 | fveq1d 6105 |
. . . . . 6
⊢ (𝑔 = 𝑒 → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘(𝐹 ++ 𝑒))‘𝑁)) |
9 | 8 | eqeq1d 2612 |
. . . . 5
⊢ (𝑔 = 𝑒 → (((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁) ↔ ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁))) |
10 | 9 | imbi2d 329 |
. . . 4
⊢ (𝑔 = 𝑒 → (((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) ↔ ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁)))) |
11 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → (𝐹 ++ 𝑔) = (𝐹 ++ (𝑒 ++ 〈“𝑘”〉))) |
12 | 11 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → (𝑇‘(𝐹 ++ 𝑔)) = (𝑇‘(𝐹 ++ (𝑒 ++ 〈“𝑘”〉)))) |
13 | 12 | fveq1d 6105 |
. . . . . 6
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘(𝐹 ++ (𝑒 ++ 〈“𝑘”〉)))‘𝑁)) |
14 | 13 | eqeq1d 2612 |
. . . . 5
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → (((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁) ↔ ((𝑇‘(𝐹 ++ (𝑒 ++ 〈“𝑘”〉)))‘𝑁) = ((𝑇‘𝐹)‘𝑁))) |
15 | 14 | imbi2d 329 |
. . . 4
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → (((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) ↔ ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ (𝑒 ++ 〈“𝑘”〉)))‘𝑁) = ((𝑇‘𝐹)‘𝑁)))) |
16 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (𝐹 ++ 𝑔) = (𝐹 ++ 𝐺)) |
17 | 16 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (𝑇‘(𝐹 ++ 𝑔)) = (𝑇‘(𝐹 ++ 𝐺))) |
18 | 17 | fveq1d 6105 |
. . . . . 6
⊢ (𝑔 = 𝐺 → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘(𝐹 ++ 𝐺))‘𝑁)) |
19 | 18 | eqeq1d 2612 |
. . . . 5
⊢ (𝑔 = 𝐺 → (((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁) ↔ ((𝑇‘(𝐹 ++ 𝐺))‘𝑁) = ((𝑇‘𝐹)‘𝑁))) |
20 | 19 | imbi2d 329 |
. . . 4
⊢ (𝑔 = 𝐺 → (((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) ↔ ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ 𝐺))‘𝑁) = ((𝑇‘𝐹)‘𝑁)))) |
21 | | ccatrid 13223 |
. . . . . . 7
⊢ (𝐹 ∈ Word ℝ →
(𝐹 ++ ∅) = 𝐹) |
22 | 21 | fveq2d 6107 |
. . . . . 6
⊢ (𝐹 ∈ Word ℝ →
(𝑇‘(𝐹 ++ ∅)) = (𝑇‘𝐹)) |
23 | 22 | fveq1d 6105 |
. . . . 5
⊢ (𝐹 ∈ Word ℝ →
((𝑇‘(𝐹 ++ ∅))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) |
24 | 23 | adantr 480 |
. . . 4
⊢ ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ ∅))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) |
25 | | simprl 790 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → 𝐹 ∈ Word ℝ) |
26 | | simpll 786 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → 𝑒 ∈ Word ℝ) |
27 | | simplr 788 |
. . . . . . . . . . . . 13
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → 𝑘 ∈ ℝ) |
28 | 27 | s1cld 13236 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → 〈“𝑘”〉 ∈ Word
ℝ) |
29 | | ccatass 13224 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Word ℝ ∧ 𝑒 ∈ Word ℝ ∧
〈“𝑘”〉
∈ Word ℝ) → ((𝐹 ++ 𝑒) ++ 〈“𝑘”〉) = (𝐹 ++ (𝑒 ++ 〈“𝑘”〉))) |
30 | 25, 26, 28, 29 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → ((𝐹 ++ 𝑒) ++ 〈“𝑘”〉) = (𝐹 ++ (𝑒 ++ 〈“𝑘”〉))) |
31 | 30 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → (𝑇‘((𝐹 ++ 𝑒) ++ 〈“𝑘”〉)) = (𝑇‘(𝐹 ++ (𝑒 ++ 〈“𝑘”〉)))) |
32 | 31 | fveq1d 6105 |
. . . . . . . . 9
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → ((𝑇‘((𝐹 ++ 𝑒) ++ 〈“𝑘”〉))‘𝑁) = ((𝑇‘(𝐹 ++ (𝑒 ++ 〈“𝑘”〉)))‘𝑁)) |
33 | | ccatcl 13212 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ Word ℝ ∧ 𝑒 ∈ Word ℝ) →
(𝐹 ++ 𝑒) ∈ Word ℝ) |
34 | 25, 26, 33 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → (𝐹 ++ 𝑒) ∈ Word ℝ) |
35 | | lencl 13179 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Word ℝ →
(#‘𝐹) ∈
ℕ0) |
36 | 25, 35 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → (#‘𝐹) ∈
ℕ0) |
37 | 36 | nn0zd 11356 |
. . . . . . . . . . . . 13
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → (#‘𝐹) ∈
ℤ) |
38 | | lencl 13179 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ++ 𝑒) ∈ Word ℝ → (#‘(𝐹 ++ 𝑒)) ∈
ℕ0) |
39 | 34, 38 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → (#‘(𝐹 ++ 𝑒)) ∈
ℕ0) |
40 | 39 | nn0zd 11356 |
. . . . . . . . . . . . 13
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → (#‘(𝐹 ++ 𝑒)) ∈ ℤ) |
41 | 36 | nn0red 11229 |
. . . . . . . . . . . . . . 15
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → (#‘𝐹) ∈
ℝ) |
42 | | lencl 13179 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 ∈ Word ℝ →
(#‘𝑒) ∈
ℕ0) |
43 | 26, 42 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → (#‘𝑒) ∈
ℕ0) |
44 | | nn0addge1 11216 |
. . . . . . . . . . . . . . 15
⊢
(((#‘𝐹) ∈
ℝ ∧ (#‘𝑒)
∈ ℕ0) → (#‘𝐹) ≤ ((#‘𝐹) + (#‘𝑒))) |
45 | 41, 43, 44 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → (#‘𝐹) ≤ ((#‘𝐹) + (#‘𝑒))) |
46 | | ccatlen 13213 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ Word ℝ ∧ 𝑒 ∈ Word ℝ) →
(#‘(𝐹 ++ 𝑒)) = ((#‘𝐹) + (#‘𝑒))) |
47 | 25, 26, 46 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → (#‘(𝐹 ++ 𝑒)) = ((#‘𝐹) + (#‘𝑒))) |
48 | 45, 47 | breqtrrd 4611 |
. . . . . . . . . . . . 13
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → (#‘𝐹) ≤ (#‘(𝐹 ++ 𝑒))) |
49 | | eluz2 11569 |
. . . . . . . . . . . . 13
⊢
((#‘(𝐹 ++
𝑒)) ∈
(ℤ≥‘(#‘𝐹)) ↔ ((#‘𝐹) ∈ ℤ ∧ (#‘(𝐹 ++ 𝑒)) ∈ ℤ ∧ (#‘𝐹) ≤ (#‘(𝐹 ++ 𝑒)))) |
50 | 37, 40, 48, 49 | syl3anbrc 1239 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → (#‘(𝐹 ++ 𝑒)) ∈
(ℤ≥‘(#‘𝐹))) |
51 | | fzoss2 12365 |
. . . . . . . . . . . 12
⊢
((#‘(𝐹 ++
𝑒)) ∈
(ℤ≥‘(#‘𝐹)) → (0..^(#‘𝐹)) ⊆ (0..^(#‘(𝐹 ++ 𝑒)))) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → (0..^(#‘𝐹)) ⊆ (0..^(#‘(𝐹 ++ 𝑒)))) |
53 | | simprr 792 |
. . . . . . . . . . 11
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → 𝑁 ∈ (0..^(#‘𝐹))) |
54 | 52, 53 | sseldd 3569 |
. . . . . . . . . 10
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → 𝑁 ∈ (0..^(#‘(𝐹 ++ 𝑒)))) |
55 | | signsv.p |
. . . . . . . . . . 11
⊢ ⨣ =
(𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦
if(𝑏 = 0, 𝑎, 𝑏)) |
56 | | signsv.w |
. . . . . . . . . . 11
⊢ 𝑊 = {〈(Base‘ndx), {-1,
0, 1}〉, 〈(+g‘ndx), ⨣
〉} |
57 | | signsv.t |
. . . . . . . . . . 11
⊢ 𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(#‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓‘𝑖)))))) |
58 | | signsv.v |
. . . . . . . . . . 11
⊢ 𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(#‘𝑓))if(((𝑇‘𝑓)‘𝑗) ≠ ((𝑇‘𝑓)‘(𝑗 − 1)), 1, 0)) |
59 | 55, 56, 57, 58 | signstfvp 29974 |
. . . . . . . . . 10
⊢ (((𝐹 ++ 𝑒) ∈ Word ℝ ∧ 𝑘 ∈ ℝ ∧ 𝑁 ∈ (0..^(#‘(𝐹 ++ 𝑒)))) → ((𝑇‘((𝐹 ++ 𝑒) ++ 〈“𝑘”〉))‘𝑁) = ((𝑇‘(𝐹 ++ 𝑒))‘𝑁)) |
60 | 34, 27, 54, 59 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → ((𝑇‘((𝐹 ++ 𝑒) ++ 〈“𝑘”〉))‘𝑁) = ((𝑇‘(𝐹 ++ 𝑒))‘𝑁)) |
61 | 32, 60 | eqtr3d 2646 |
. . . . . . . 8
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → ((𝑇‘(𝐹 ++ (𝑒 ++ 〈“𝑘”〉)))‘𝑁) = ((𝑇‘(𝐹 ++ 𝑒))‘𝑁)) |
62 | 61 | adantr 480 |
. . . . . . 7
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) ∧ ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) → ((𝑇‘(𝐹 ++ (𝑒 ++ 〈“𝑘”〉)))‘𝑁) = ((𝑇‘(𝐹 ++ 𝑒))‘𝑁)) |
63 | | simpr 476 |
. . . . . . 7
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) ∧ ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) → ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) |
64 | 62, 63 | eqtrd 2644 |
. . . . . 6
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) ∧ ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) → ((𝑇‘(𝐹 ++ (𝑒 ++ 〈“𝑘”〉)))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) |
65 | 64 | exp31 628 |
. . . . 5
⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → (((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁) → ((𝑇‘(𝐹 ++ (𝑒 ++ 〈“𝑘”〉)))‘𝑁) = ((𝑇‘𝐹)‘𝑁)))) |
66 | 65 | a2d 29 |
. . . 4
⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) → ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ (𝑒 ++ 〈“𝑘”〉)))‘𝑁) = ((𝑇‘𝐹)‘𝑁)))) |
67 | 5, 10, 15, 20, 24, 66 | wrdind 13328 |
. . 3
⊢ (𝐺 ∈ Word ℝ →
((𝐹 ∈ Word ℝ
∧ 𝑁 ∈
(0..^(#‘𝐹))) →
((𝑇‘(𝐹 ++ 𝐺))‘𝑁) = ((𝑇‘𝐹)‘𝑁))) |
68 | 67 | 3impib 1254 |
. 2
⊢ ((𝐺 ∈ Word ℝ ∧ 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ 𝐺))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) |
69 | 68 | 3com12 1261 |
1
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐺 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ 𝐺))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) |