let i be Element of NAT ; :: thesis: for p being FinSequence holds Seq (i Shift p) = p
let p be FinSequence; :: thesis: Seq (i Shift p) = p
A1: dom (Seq (i Shift p)) = dom p by Th58;
for x being set st x in dom p holds
(Seq (i Shift p)) . x = p . x by Th60;
hence Seq (i Shift p) = p by A1, FUNCT_1:9; :: thesis: verum