theorem Th20: :: AMI_8:20

for m, n being Nat
for s being State of SCM
for P being Instruction-Sequence of SCM st IterativeAlgorithm (SubFrom ((dl. m),(dl. n))) c= P holds
for k being Nat st IC (Comput (P,s,k)) = 2 holds
( IC (Comput (P,s,(k + 1))) = 3 & (Comput (P,s,(k + 1))) . (dl. m) = ((Comput (P,s,k)) . (dl. m)) - ((Comput (P,s,k)) . (dl. n)) & ( for j being Nat st j <> m holds
(Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) ) )