for S being COM-Struct
for n being Nat
for I being Program of S holds (Shift ((stop I),n)) . n = (Shift (I,n)) . n