Description: The last symbol of a word concatenated with the empty word is the last symbol of the word. (Contributed by AV, 22-Oct-2018) (Proof shortened by AV, 1-May-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | lswccat0lsw | |- ( W e. Word V -> ( lastS ` ( W ++ (/) ) ) = ( lastS ` W ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ccatrid | |- ( W e. Word V -> ( W ++ (/) ) = W ) |
|
| 2 | 1 | fveq2d | |- ( W e. Word V -> ( lastS ` ( W ++ (/) ) ) = ( lastS ` W ) ) |