theorem :: FINSEQ_1:97

for q being FinSubsequence holds
( q = {} iff Seq q = {} ) by Lm6;