let S be COM-Struct ; for n being Nat
for I being Program of S holds (Shift ((stop I),n)) . n = (Shift (I,n)) . n
let n be Nat; for I being Program of S holds (Shift ((stop I),n)) . n = (Shift (I,n)) . n
let I be Program of S; (Shift ((stop I),n)) . n = (Shift (I,n)) . n
A1:
0 in dom I
by AFINSQ_1:66;
thus (Shift ((stop I),n)) . n =
(Shift (I,n)) . (0 + n)
by A1, Th49
.=
(Shift (I,n)) . n
; verum