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	$$⊢\mathrm{lastS}\left(\varnothing \right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		wrd0	$$⊢\varnothing \in \mathrm{Word}V$$
2		hash0	$$⊢\left|\varnothing \right|=0$$
3		lsw0	$$⊢\left(\varnothing \in \mathrm{Word}V\wedge \left|\varnothing \right|=0\right)\to \mathrm{lastS}\left(\varnothing \right)=\varnothing$$
4	1 2 3	mp2an	$$⊢\mathrm{lastS}\left(\varnothing \right)=\varnothing$$