let ins be Instruction of SCM+FSA ; :: thesis: ( InsCode ins = 4 implies ex da, db being Int-Location st ins = MultBy da,db )
assume A1: InsCode ins = 4 ; :: thesis: ex da, db being Int-Location st ins = MultBy da,db
then reconsider I = ins as Instruction of SCM by Th34;
consider A, B being Data-Location such that
A2: I = MultBy A,B by A1, AMI_5:50;
( A in SCM-Data-Loc & B in SCM-Data-Loc ) by AMI_3:def 2;
then reconsider da = A, db = B as Int-Location by Def4;
take da ; :: thesis: ex db being Int-Location st ins = MultBy da,db
take db ; :: thesis: ins = MultBy da,db
thus ins = MultBy da,db by A2, Def14; :: thesis: verum