let i be Element of NAT ; :: thesis: for q being FinSubsequence holds Seq q = Seq (i Shift q)
let q be FinSubsequence; :: thesis: Seq q = Seq (i Shift q)
A1: dom (Seq q) = dom (Seq (i Shift q)) by Th74;
for x being set st x in dom (Seq q) holds
(Seq (i Shift q)) . x = (Seq q) . x by Th76;
hence Seq q = Seq (i Shift q) by A1, FUNCT_1:9; :: thesis: verum