theorem :: FINSEQ_3:158

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