for p being FinSubsequence holds card p = len (Seq p)