| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | hasheq0 14402 | . . . . . . . . . . 11
⊢ (𝑤 ∈ V →
((♯‘𝑤) = 0
↔ 𝑤 =
∅)) | 
| 2 | 1 | elv 3485 | . . . . . . . . . 10
⊢
((♯‘𝑤) =
0 ↔ 𝑤 =
∅) | 
| 3 | 2 | biimpri 228 | . . . . . . . . 9
⊢ (𝑤 = ∅ →
(♯‘𝑤) =
0) | 
| 4 | 3 | oveq2d 7447 | . . . . . . . 8
⊢ (𝑤 = ∅ →
(0..^(♯‘𝑤)) =
(0..^0)) | 
| 5 |  | fzo0 13723 | . . . . . . . 8
⊢ (0..^0) =
∅ | 
| 6 | 4, 5 | eqtrdi 2793 | . . . . . . 7
⊢ (𝑤 = ∅ →
(0..^(♯‘𝑤)) =
∅) | 
| 7 |  | fveq1 6905 | . . . . . . . . 9
⊢ (𝑤 = ∅ → (𝑤‘𝑖) = (∅‘𝑖)) | 
| 8 | 7 | fveq1d 6908 | . . . . . . . 8
⊢ (𝑤 = ∅ → ((𝑤‘𝑖)‘𝐾) = ((∅‘𝑖)‘𝐾)) | 
| 9 | 8 | eqeq1d 2739 | . . . . . . 7
⊢ (𝑤 = ∅ → (((𝑤‘𝑖)‘𝐾) = 𝐾 ↔ ((∅‘𝑖)‘𝐾) = 𝐾)) | 
| 10 | 6, 9 | raleqbidv 3346 | . . . . . 6
⊢ (𝑤 = ∅ → (∀𝑖 ∈
(0..^(♯‘𝑤))((𝑤‘𝑖)‘𝐾) = 𝐾 ↔ ∀𝑖 ∈ ∅ ((∅‘𝑖)‘𝐾) = 𝐾)) | 
| 11 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑤 = ∅ → (𝑆 Σg
𝑤) = (𝑆 Σg
∅)) | 
| 12 | 11 | fveq1d 6908 | . . . . . . 7
⊢ (𝑤 = ∅ → ((𝑆 Σg
𝑤)‘𝐾) = ((𝑆 Σg
∅)‘𝐾)) | 
| 13 | 12 | eqeq1d 2739 | . . . . . 6
⊢ (𝑤 = ∅ → (((𝑆 Σg
𝑤)‘𝐾) = 𝐾 ↔ ((𝑆 Σg
∅)‘𝐾) = 𝐾)) | 
| 14 | 10, 13 | imbi12d 344 | . . . . 5
⊢ (𝑤 = ∅ →
((∀𝑖 ∈
(0..^(♯‘𝑤))((𝑤‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑤)‘𝐾) = 𝐾) ↔ (∀𝑖 ∈ ∅ ((∅‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg
∅)‘𝐾) = 𝐾))) | 
| 15 | 14 | imbi2d 340 | . . . 4
⊢ (𝑤 = ∅ → (((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (∀𝑖 ∈ (0..^(♯‘𝑤))((𝑤‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑤)‘𝐾) = 𝐾)) ↔ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (∀𝑖 ∈ ∅ ((∅‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg
∅)‘𝐾) = 𝐾)))) | 
| 16 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑤 = 𝑦 → (♯‘𝑤) = (♯‘𝑦)) | 
| 17 | 16 | oveq2d 7447 | . . . . . . 7
⊢ (𝑤 = 𝑦 → (0..^(♯‘𝑤)) = (0..^(♯‘𝑦))) | 
| 18 |  | fveq1 6905 | . . . . . . . . 9
⊢ (𝑤 = 𝑦 → (𝑤‘𝑖) = (𝑦‘𝑖)) | 
| 19 | 18 | fveq1d 6908 | . . . . . . . 8
⊢ (𝑤 = 𝑦 → ((𝑤‘𝑖)‘𝐾) = ((𝑦‘𝑖)‘𝐾)) | 
| 20 | 19 | eqeq1d 2739 | . . . . . . 7
⊢ (𝑤 = 𝑦 → (((𝑤‘𝑖)‘𝐾) = 𝐾 ↔ ((𝑦‘𝑖)‘𝐾) = 𝐾)) | 
| 21 | 17, 20 | raleqbidv 3346 | . . . . . 6
⊢ (𝑤 = 𝑦 → (∀𝑖 ∈ (0..^(♯‘𝑤))((𝑤‘𝑖)‘𝐾) = 𝐾 ↔ ∀𝑖 ∈ (0..^(♯‘𝑦))((𝑦‘𝑖)‘𝐾) = 𝐾)) | 
| 22 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑤 = 𝑦 → (𝑆 Σg 𝑤) = (𝑆 Σg 𝑦)) | 
| 23 | 22 | fveq1d 6908 | . . . . . . 7
⊢ (𝑤 = 𝑦 → ((𝑆 Σg 𝑤)‘𝐾) = ((𝑆 Σg 𝑦)‘𝐾)) | 
| 24 | 23 | eqeq1d 2739 | . . . . . 6
⊢ (𝑤 = 𝑦 → (((𝑆 Σg 𝑤)‘𝐾) = 𝐾 ↔ ((𝑆 Σg 𝑦)‘𝐾) = 𝐾)) | 
| 25 | 21, 24 | imbi12d 344 | . . . . 5
⊢ (𝑤 = 𝑦 → ((∀𝑖 ∈ (0..^(♯‘𝑤))((𝑤‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑤)‘𝐾) = 𝐾) ↔ (∀𝑖 ∈ (0..^(♯‘𝑦))((𝑦‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑦)‘𝐾) = 𝐾))) | 
| 26 | 25 | imbi2d 340 | . . . 4
⊢ (𝑤 = 𝑦 → (((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (∀𝑖 ∈ (0..^(♯‘𝑤))((𝑤‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑤)‘𝐾) = 𝐾)) ↔ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (∀𝑖 ∈ (0..^(♯‘𝑦))((𝑦‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑦)‘𝐾) = 𝐾)))) | 
| 27 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑤 = (𝑦 ++ 〈“𝑧”〉) → (♯‘𝑤) = (♯‘(𝑦 ++ 〈“𝑧”〉))) | 
| 28 | 27 | oveq2d 7447 | . . . . . . 7
⊢ (𝑤 = (𝑦 ++ 〈“𝑧”〉) →
(0..^(♯‘𝑤)) =
(0..^(♯‘(𝑦 ++
〈“𝑧”〉)))) | 
| 29 |  | fveq1 6905 | . . . . . . . . 9
⊢ (𝑤 = (𝑦 ++ 〈“𝑧”〉) → (𝑤‘𝑖) = ((𝑦 ++ 〈“𝑧”〉)‘𝑖)) | 
| 30 | 29 | fveq1d 6908 | . . . . . . . 8
⊢ (𝑤 = (𝑦 ++ 〈“𝑧”〉) → ((𝑤‘𝑖)‘𝐾) = (((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾)) | 
| 31 | 30 | eqeq1d 2739 | . . . . . . 7
⊢ (𝑤 = (𝑦 ++ 〈“𝑧”〉) → (((𝑤‘𝑖)‘𝐾) = 𝐾 ↔ (((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾)) | 
| 32 | 28, 31 | raleqbidv 3346 | . . . . . 6
⊢ (𝑤 = (𝑦 ++ 〈“𝑧”〉) → (∀𝑖 ∈
(0..^(♯‘𝑤))((𝑤‘𝑖)‘𝐾) = 𝐾 ↔ ∀𝑖 ∈ (0..^(♯‘(𝑦 ++ 〈“𝑧”〉)))(((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾)) | 
| 33 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑤 = (𝑦 ++ 〈“𝑧”〉) → (𝑆 Σg 𝑤) = (𝑆 Σg (𝑦 ++ 〈“𝑧”〉))) | 
| 34 | 33 | fveq1d 6908 | . . . . . . 7
⊢ (𝑤 = (𝑦 ++ 〈“𝑧”〉) → ((𝑆 Σg 𝑤)‘𝐾) = ((𝑆 Σg (𝑦 ++ 〈“𝑧”〉))‘𝐾)) | 
| 35 | 34 | eqeq1d 2739 | . . . . . 6
⊢ (𝑤 = (𝑦 ++ 〈“𝑧”〉) → (((𝑆 Σg 𝑤)‘𝐾) = 𝐾 ↔ ((𝑆 Σg (𝑦 ++ 〈“𝑧”〉))‘𝐾) = 𝐾)) | 
| 36 | 32, 35 | imbi12d 344 | . . . . 5
⊢ (𝑤 = (𝑦 ++ 〈“𝑧”〉) → ((∀𝑖 ∈
(0..^(♯‘𝑤))((𝑤‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑤)‘𝐾) = 𝐾) ↔ (∀𝑖 ∈ (0..^(♯‘(𝑦 ++ 〈“𝑧”〉)))(((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg (𝑦 ++ 〈“𝑧”〉))‘𝐾) = 𝐾))) | 
| 37 | 36 | imbi2d 340 | . . . 4
⊢ (𝑤 = (𝑦 ++ 〈“𝑧”〉) → (((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (∀𝑖 ∈ (0..^(♯‘𝑤))((𝑤‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑤)‘𝐾) = 𝐾)) ↔ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (∀𝑖 ∈ (0..^(♯‘(𝑦 ++ 〈“𝑧”〉)))(((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg (𝑦 ++ 〈“𝑧”〉))‘𝐾) = 𝐾)))) | 
| 38 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑤 = 𝑊 → (♯‘𝑤) = (♯‘𝑊)) | 
| 39 | 38 | oveq2d 7447 | . . . . . . 7
⊢ (𝑤 = 𝑊 → (0..^(♯‘𝑤)) = (0..^(♯‘𝑊))) | 
| 40 |  | fveq1 6905 | . . . . . . . . 9
⊢ (𝑤 = 𝑊 → (𝑤‘𝑖) = (𝑊‘𝑖)) | 
| 41 | 40 | fveq1d 6908 | . . . . . . . 8
⊢ (𝑤 = 𝑊 → ((𝑤‘𝑖)‘𝐾) = ((𝑊‘𝑖)‘𝐾)) | 
| 42 | 41 | eqeq1d 2739 | . . . . . . 7
⊢ (𝑤 = 𝑊 → (((𝑤‘𝑖)‘𝐾) = 𝐾 ↔ ((𝑊‘𝑖)‘𝐾) = 𝐾)) | 
| 43 | 39, 42 | raleqbidv 3346 | . . . . . 6
⊢ (𝑤 = 𝑊 → (∀𝑖 ∈ (0..^(♯‘𝑤))((𝑤‘𝑖)‘𝐾) = 𝐾 ↔ ∀𝑖 ∈ (0..^(♯‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾)) | 
| 44 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑤 = 𝑊 → (𝑆 Σg 𝑤) = (𝑆 Σg 𝑊)) | 
| 45 | 44 | fveq1d 6908 | . . . . . . 7
⊢ (𝑤 = 𝑊 → ((𝑆 Σg 𝑤)‘𝐾) = ((𝑆 Σg 𝑊)‘𝐾)) | 
| 46 | 45 | eqeq1d 2739 | . . . . . 6
⊢ (𝑤 = 𝑊 → (((𝑆 Σg 𝑤)‘𝐾) = 𝐾 ↔ ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) | 
| 47 | 43, 46 | imbi12d 344 | . . . . 5
⊢ (𝑤 = 𝑊 → ((∀𝑖 ∈ (0..^(♯‘𝑤))((𝑤‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑤)‘𝐾) = 𝐾) ↔ (∀𝑖 ∈ (0..^(♯‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾))) | 
| 48 | 47 | imbi2d 340 | . . . 4
⊢ (𝑤 = 𝑊 → (((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (∀𝑖 ∈ (0..^(♯‘𝑤))((𝑤‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑤)‘𝐾) = 𝐾)) ↔ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (∀𝑖 ∈ (0..^(♯‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)))) | 
| 49 |  | eqid 2737 | . . . . . . . . 9
⊢
(0g‘𝑆) = (0g‘𝑆) | 
| 50 | 49 | gsum0 18697 | . . . . . . . 8
⊢ (𝑆 Σg
∅) = (0g‘𝑆) | 
| 51 |  | gsmsymgrfix.s | . . . . . . . . . 10
⊢ 𝑆 = (SymGrp‘𝑁) | 
| 52 | 51 | symgid 19419 | . . . . . . . . 9
⊢ (𝑁 ∈ Fin → ( I ↾
𝑁) =
(0g‘𝑆)) | 
| 53 | 52 | adantr 480 | . . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → ( I ↾ 𝑁) = (0g‘𝑆)) | 
| 54 | 50, 53 | eqtr4id 2796 | . . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (𝑆 Σg ∅) = ( I
↾ 𝑁)) | 
| 55 | 54 | fveq1d 6908 | . . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → ((𝑆 Σg
∅)‘𝐾) = (( I
↾ 𝑁)‘𝐾)) | 
| 56 |  | fvresi 7193 | . . . . . . 7
⊢ (𝐾 ∈ 𝑁 → (( I ↾ 𝑁)‘𝐾) = 𝐾) | 
| 57 | 56 | adantl 481 | . . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (( I ↾ 𝑁)‘𝐾) = 𝐾) | 
| 58 | 55, 57 | eqtrd 2777 | . . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → ((𝑆 Σg
∅)‘𝐾) = 𝐾) | 
| 59 | 58 | a1d 25 | . . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (∀𝑖 ∈ ∅ ((∅‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg
∅)‘𝐾) = 𝐾)) | 
| 60 |  | ccatws1len 14658 | . . . . . . . . . . 11
⊢ (𝑦 ∈ Word 𝐵 → (♯‘(𝑦 ++ 〈“𝑧”〉)) = ((♯‘𝑦) + 1)) | 
| 61 | 60 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑦 ∈ Word 𝐵 → (0..^(♯‘(𝑦 ++ 〈“𝑧”〉))) =
(0..^((♯‘𝑦) +
1))) | 
| 62 | 61 | raleqdv 3326 | . . . . . . . . 9
⊢ (𝑦 ∈ Word 𝐵 → (∀𝑖 ∈ (0..^(♯‘(𝑦 ++ 〈“𝑧”〉)))(((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾 ↔ ∀𝑖 ∈ (0..^((♯‘𝑦) + 1))(((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾)) | 
| 63 | 62 | adantr 480 | . . . . . . . 8
⊢ ((𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵) → (∀𝑖 ∈ (0..^(♯‘(𝑦 ++ 〈“𝑧”〉)))(((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾 ↔ ∀𝑖 ∈ (0..^((♯‘𝑦) + 1))(((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾)) | 
| 64 | 63 | adantr 480 | . . . . . . 7
⊢ (((𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(♯‘𝑦))((𝑦‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑦)‘𝐾) = 𝐾))) → (∀𝑖 ∈ (0..^(♯‘(𝑦 ++ 〈“𝑧”〉)))(((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾 ↔ ∀𝑖 ∈ (0..^((♯‘𝑦) + 1))(((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾)) | 
| 65 |  | gsmsymgrfix.b | . . . . . . . . 9
⊢ 𝐵 = (Base‘𝑆) | 
| 66 | 51, 65 | gsmsymgrfixlem1 19445 | . . . . . . . 8
⊢ (((𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(♯‘𝑦))((𝑦‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑦)‘𝐾) = 𝐾)) → (∀𝑖 ∈ (0..^((♯‘𝑦) + 1))(((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg (𝑦 ++ 〈“𝑧”〉))‘𝐾) = 𝐾)) | 
| 67 | 66 | 3expb 1121 | . . . . . . 7
⊢ (((𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(♯‘𝑦))((𝑦‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑦)‘𝐾) = 𝐾))) → (∀𝑖 ∈ (0..^((♯‘𝑦) + 1))(((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg (𝑦 ++ 〈“𝑧”〉))‘𝐾) = 𝐾)) | 
| 68 | 64, 67 | sylbid 240 | . . . . . 6
⊢ (((𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(♯‘𝑦))((𝑦‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑦)‘𝐾) = 𝐾))) → (∀𝑖 ∈ (0..^(♯‘(𝑦 ++ 〈“𝑧”〉)))(((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg (𝑦 ++ 〈“𝑧”〉))‘𝐾) = 𝐾)) | 
| 69 | 68 | exp32 420 | . . . . 5
⊢ ((𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → ((∀𝑖 ∈ (0..^(♯‘𝑦))((𝑦‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑦)‘𝐾) = 𝐾) → (∀𝑖 ∈ (0..^(♯‘(𝑦 ++ 〈“𝑧”〉)))(((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg (𝑦 ++ 〈“𝑧”〉))‘𝐾) = 𝐾)))) | 
| 70 | 69 | a2d 29 | . . . 4
⊢ ((𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵) → (((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (∀𝑖 ∈ (0..^(♯‘𝑦))((𝑦‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑦)‘𝐾) = 𝐾)) → ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (∀𝑖 ∈ (0..^(♯‘(𝑦 ++ 〈“𝑧”〉)))(((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg (𝑦 ++ 〈“𝑧”〉))‘𝐾) = 𝐾)))) | 
| 71 | 15, 26, 37, 48, 59, 70 | wrdind 14760 | . . 3
⊢ (𝑊 ∈ Word 𝐵 → ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (∀𝑖 ∈ (0..^(♯‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾))) | 
| 72 | 71 | com12 32 | . 2
⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (𝑊 ∈ Word 𝐵 → (∀𝑖 ∈ (0..^(♯‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾))) | 
| 73 | 72 | 3impia 1118 | 1
⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ∧ 𝑊 ∈ Word 𝐵) → (∀𝑖 ∈ (0..^(♯‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) |