let S be COM-Struct ; :: thesis: for n being Nat
for I being Program of S
for loc being Nat st loc in dom I holds
(Shift ((stop I),n)) . (loc + n) = (Shift (I,n)) . (loc + n)
let n be Nat; :: thesis: for I being Program of S
for loc being Nat st loc in dom I holds
(Shift ((stop I),n)) . (loc + n) = (Shift (I,n)) . (loc + n)
let I be Program of S; :: thesis: for loc being Nat st loc in dom I holds
(Shift ((stop I),n)) . (loc + n) = (Shift (I,n)) . (loc + n)
let loc be Nat; :: 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:21;
reconsider l = loc as Element of NAT by ORDINAL1:def 12;
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 3
.= (Shift ((stop I),n)) . (loc + n) by A2, A1, VALUED_1:def 12 ;
:: thesis: verum