theorem Th23: :: SCMFSA_2:30

for ins being Instruction of SCM+FSA st InsCode ins = 1 holds
ex da, db being Int-Location st ins = da := db