let i be Nat; :: thesis: for q being FinSubsequence holds Seq q = Seq (Shift (q,i))
let q be FinSubsequence; :: thesis: Seq q = Seq (Shift (q,i))
A1: dom (Seq q) = dom (Seq (Shift (q,i))) by Th55;
for x being object st x in dom (Seq q) holds
(Seq (Shift (q,i))) . x = (Seq q) . x by Th57;
hence Seq q = Seq (Shift (q,i)) by A1; :: thesis: verum