| Step |
Hyp |
Ref |
Expression |
| 1 |
|
s4s2 |
|- <" A B C D E F "> = ( <" A B C D "> ++ <" E F "> ) |
| 2 |
1
|
eqcomi |
|- ( <" A B C D "> ++ <" E F "> ) = <" A B C D E F "> |
| 3 |
2
|
oveq1i |
|- ( ( <" A B C D "> ++ <" E F "> ) ++ <" G "> ) = ( <" A B C D E F "> ++ <" G "> ) |
| 4 |
|
s4cli |
|- <" A B C D "> e. Word _V |
| 5 |
|
s1cli |
|- <" G "> e. Word _V |
| 6 |
|
df-s5 |
|- <" A B C D E "> = ( <" A B C D "> ++ <" E "> ) |
| 7 |
|
df-s2 |
|- <" F G "> = ( <" F "> ++ <" G "> ) |
| 8 |
4 5 6 7
|
cats2cat |
|- ( <" A B C D E "> ++ <" F G "> ) = ( ( <" A B C D "> ++ <" E F "> ) ++ <" G "> ) |
| 9 |
|
df-s7 |
|- <" A B C D E F G "> = ( <" A B C D E F "> ++ <" G "> ) |
| 10 |
3 8 9
|
3eqtr4ri |
|- <" A B C D E F G "> = ( <" A B C D E "> ++ <" F G "> ) |