theorem Th41: :: VALUED_1:42

for i being Nat
for q being FinSubsequence holds card q = card (Shift (q,i))