theorem Th25: :: SCMFSA_2:32

for ins being Instruction of SCM+FSA st InsCode ins = 3 holds
ex da, db being Int-Location st ins = SubFrom (da,db)