let i be Nat; :: thesis: for p being FinSequence holds Seq (Shift (p,i)) = p
let p be FinSequence; :: thesis: Seq (Shift (p,i)) = p
A1: dom (Seq (Shift (p,i))) = dom p by Th42;
for x being object st x in dom p holds
(Seq (Shift (p,i))) . x = p . x by Th44;
hence Seq (Shift (p,i)) = p by A1; :: thesis: verum