let ins be Instruction of SCM+FSA; :: thesis: ( InsCode ins = 3 implies ex da, db being Int-Location st ins = SubFrom (da,db) )
assume A1: InsCode ins = 3 ; :: thesis: ex da, db being Int-Location st ins = SubFrom (da,db)
then reconsider I = ins as Instruction of SCM by Th8;
consider A, B being Data-Location such that
A2: I = SubFrom (A,B) by A1, AMI_5:10;
A3: Int-Locations = SCM+FSA-Data-Loc ;
( A in SCM-Data-Loc & B in SCM-Data-Loc ) by AMI_2:def 16;
then reconsider da = A, db = B as Int-Location by A3;
take da ; :: thesis: ex db being Int-Location st ins = SubFrom (da,db)
take db ; :: thesis: ins = SubFrom (da,db)
thus ins = SubFrom (da,db) by A2, Def8; :: thesis: verum