Step |
Hyp |
Ref |
Expression |
1 |
|
simpl |
|- ( ( W e. Word V /\ S e. V ) -> W e. Word V ) |
2 |
|
s1cl |
|- ( S e. V -> <" S "> e. Word V ) |
3 |
2
|
adantl |
|- ( ( W e. Word V /\ S e. V ) -> <" S "> e. Word V ) |
4 |
|
s1nz |
|- <" S "> =/= (/) |
5 |
4
|
a1i |
|- ( ( W e. Word V /\ S e. V ) -> <" S "> =/= (/) ) |
6 |
|
lswccatn0lsw |
|- ( ( W e. Word V /\ <" S "> e. Word V /\ <" S "> =/= (/) ) -> ( lastS ` ( W ++ <" S "> ) ) = ( lastS ` <" S "> ) ) |
7 |
1 3 5 6
|
syl3anc |
|- ( ( W e. Word V /\ S e. V ) -> ( lastS ` ( W ++ <" S "> ) ) = ( lastS ` <" S "> ) ) |
8 |
|
lsws1 |
|- ( S e. V -> ( lastS ` <" S "> ) = S ) |
9 |
8
|
adantl |
|- ( ( W e. Word V /\ S e. V ) -> ( lastS ` <" S "> ) = S ) |
10 |
7 9
|
eqtrd |
|- ( ( W e. Word V /\ S e. V ) -> ( lastS ` ( W ++ <" S "> ) ) = S ) |