let j, m, n be Nat; :: thesis: ( m <> j implies AddTo ((dl. m),(dl. n)) is j -dl.constant )
assume A1: m <> j ; :: thesis: AddTo ((dl. m),(dl. n)) is j -dl.constant
let P be Instruction-Sequence of SCM; :: according to AMI_8:def 3 :: thesis: for s being State of SCM
for k being Nat st CurInstr (P,(Comput (P,s,k))) = AddTo ((dl. m),(dl. n)) holds
(Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j)
let s be State of SCM; :: thesis: for k being Nat st CurInstr (P,(Comput (P,s,k))) = AddTo ((dl. m),(dl. n)) holds
(Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j)
let k be Nat; :: thesis: ( CurInstr (P,(Comput (P,s,k))) = AddTo ((dl. m),(dl. n)) implies (Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) )
Comput (P,s,(k + 1)) = Following (P,(Comput (P,s,k))) by EXTPRO_1:3;
hence ( CurInstr (P,(Comput (P,s,k))) = AddTo ((dl. m),(dl. n)) implies (Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) ) by A1, AMI_3:3, AMI_3:10; :: thesis: verum