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