theorem Th7: :: SCM_1:7

for F being NAT -defined the InstructionsF of SCM -valued total Function
for k, n being Element of NAT
for s being State of SCM
for a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = MultBy (a,b) holds
( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) * ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a holds
(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )