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 AFINSQ_1:24;
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, AFINSQ_1:def 4
.= (Shift ((stop I),n)) . (loc + n) by A2, A1, VALUED_1:def 12 ;
:: thesis: verum