let n be Element of NAT ; :: thesis: for I being Program of SCMPDS holds (Shift ((stop I),n)) . n = (Shift (I,n)) . n
let I be Program of SCMPDS; :: thesis: (Shift ((stop I),n)) . n = (Shift (I,n)) . n
card I > 0 ;
then A1: 0 in dom I by AFINSQ_1:70;
thus (Shift ((stop I),n)) . n = (Shift ((stop I),n)) . (0 + n)
.= (Shift ((stop I),n)) . (0 + n)
.= (Shift (I,n)) . (0 + n) by A1, Th18
.= (Shift (I,n)) . (0 + n)
.= (Shift (I,n)) . n ; :: thesis: verum