theorem :: REWRITE1:5

for p being FinSequence st p <> {} holds
ex x being object ex q being FinSequence st
( p = <*x*> ^ q & len p = (len q) + 1 )