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)
consider ss being FinSubsequence such that
A1: ( 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;
A2: dom q, dom (i Shift q) are_equipotent by A1, WELLORD2:def 4;
( card (dom q) = card q & card (dom (i Shift q)) = card (i Shift q) ) by CARD_1:104;
hence card q = card (i Shift q) by A2, CARD_1:21; :: thesis: verum