let i be Element of NAT ; :: thesis: for q being FinSubsequence holds dom (Seq q) = dom (Seq (i Shift q))
let q be FinSubsequence; :: thesis: dom (Seq q) = dom (Seq (i Shift q))
A1: card q = card (i Shift q) by Th57;
A2: len (Seq q) = card q by Th7;
A3: len (Seq (i Shift q)) = card (i Shift q) by Th7;
thus dom (Seq q) = Seg (len (Seq q)) by FINSEQ_1:def 3
.= dom (Seq (i Shift q)) by A1, A2, A3, FINSEQ_1:def 3 ; :: thesis: verum