let i be Nat; :: thesis: for q being FinSubsequence holds card q = card (Shift (q,i))
let q be FinSubsequence; :: thesis: card q = card (Shift (q,i))
ex ss being FinSubsequence st
( dom ss = dom q & rng ss = dom (Shift (q,i)) & ( for k being Element of NAT st k in dom q holds
ss . k = i + k ) & ss is one-to-one ) by Th40;
then A1: dom q, dom (Shift (q,i)) are_equipotent ;
A2: card (dom q) = card q by CARD_1:62;
card (dom (Shift (q,i))) = card (Shift (q,i)) by CARD_1:62;
hence card q = card (Shift (q,i)) by A1, A2, CARD_1:5; :: thesis: verum