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 ) ) |