Theorem lsw0g

Description: The last symbol of an empty word does not exist. (Contributed by Alexander van der Vekens, 11-Nov-2018)

	Ref	Expression
Assertion	lsw0g	⊢ ( lastS ‘ ∅ ) = ∅

Proof

Step	Hyp	Ref	Expression
1		wrd0	⊢ ∅ ∈ Word 𝑉
2		hash0	⊢ ( ♯ ‘ ∅ ) = 0
3		lsw0	⊢ ( ( ∅ ∈ Word 𝑉 ∧ ( ♯ ‘ ∅ ) = 0 ) → ( lastS ‘ ∅ ) = ∅ )
4	1 2 3	mp2an	⊢ ( lastS ‘ ∅ ) = ∅