let S be COM-Struct ; :: thesis: for n being Nat
for I being Program of S holds (Shift ((stop I),n)) . n = (Shift (I,n)) . n
let n be Nat; :: thesis: for I being Program of S holds (Shift ((stop I),n)) . n = (Shift (I,n)) . n
let I be Program of S; :: thesis: (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 ; :: thesis: verum