let i be Nat; :: thesis: for q being FinSubsequence holds dom (Seq q) = dom (Seq (Shift (q,i)))
let q be FinSubsequence; :: thesis: dom (Seq q) = dom (Seq (Shift (q,i)))
A1: len (Seq q) = card q by FINSEQ_3:158;
A2: len (Seq (Shift (q,i))) = card (Shift (q,i)) by FINSEQ_3:158;
thus dom (Seq q) = Seg (len (Seq q)) by FINSEQ_1:def 3
.= dom (Seq (Shift (q,i))) by Th41, A1, A2, FINSEQ_1:def 3 ; :: thesis: verum