Definition df-s7

Description: Define the length 7 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016)

	Ref	Expression
Assertion	df-s7	⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 ”⟩ ++ ⟨“ 𝐺 ”⟩ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2		cC	⊢ 𝐶
3		cD	⊢ 𝐷
4		cE	⊢ 𝐸
5		cF	⊢ 𝐹
6		cG	⊢ 𝐺
7	0 1 2 3 4 5 6	cs7	⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩
8	0 1 2 3 4 5	cs6	⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 ”⟩
9		cconcat	⊢ ++
10	6	cs1	⊢ ⟨“ 𝐺 ”⟩
11	8 10 9	co	⊢ ( ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 ”⟩ ++ ⟨“ 𝐺 ”⟩ )
12	7 11	wceq	⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 ”⟩ ++ ⟨“ 𝐺 ”⟩ )