let n be Nat; :: thesis: for S being COM-Struct
for I being Program of S holds (Shift ((stop I),n)) . n = (Shift (I,n)) . n
let S be COM-Struct ; :: 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
card I > 0 ;
then A1: 0 in dom I by AFINSQ_1:66;
thus (Shift ((stop I),n)) . n = (Shift (I,n)) . (0 + n) by A1, Th18
.= (Shift (I,n)) . n ; :: thesis: verum