theorem Th2: :: REWRITE3:2

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