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