theorem :: FINSEQ_1:20

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