Theorem s7len

Description: The length of a length 7 string. (Contributed by Mario Carneiro, 26-Feb-2016)

	Ref	Expression
Assertion	s7len	|- ( # ` <" A B C D E F G "> ) = 7

Proof

Step	Hyp	Ref	Expression
1		df-s7	|- <" A B C D E F G "> = ( <" A B C D E F "> ++ <" G "> )
2		s6cli	|- <" A B C D E F "> e. Word _V
3		s6len	|- ( # ` <" A B C D E F "> ) = 6
4		6p1e7	|- ( 6 + 1 ) = 7
5	1 2 3 4	cats1len	|- ( # ` <" A B C D E F G "> ) = 7