for p being FinSequence holds
( p <> {} iff len p >= 1 )