let n, loc be Element of NAT ; :: thesis: for I being Program of SCMPDS st loc in dom I holds
(Shift (stop I),n) . (loc + n) = (Shift I,n) . (loc + n)
let I be Program of SCMPDS ; :: thesis: ( loc in dom I implies (Shift (stop I),n) . (loc + n) = (Shift I,n) . (loc + n) )
A1: dom I c= dom (stop I) by SCMPDS_4:39;
reconsider l = loc as Element of NAT ;
assume A2: loc in dom I ; :: thesis: (Shift (stop I),n) . (loc + n) = (Shift I,n) . (loc + n)
hence (Shift I,n) . (loc + n) = I . l by VALUED_1:def 12
.= (stop I) . l by A2, SCMPDS_4:37
.= (Shift (stop I),n) . (loc + n) by A2, A1, VALUED_1:def 12 ;
:: thesis: verum