for p being FinSequence st p <> {} holds
ex q being FinSequence ex x being object st p = q ^ <*x*>