let ins be Instruction of SCM+FSA; :: thesis: ( InsCode ins = 13 implies ex a being Int-Location st ins = a :==1 )
assume A1: InsCode ins = 13 ; :: thesis: ex a being Int-Location st ins = a :==1

B2: now

assume ins in { [L,{},<*dB,fA,dA*>] where L is Element of Segm 14, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } ; :: thesis: contradiction
then consider K being Element of Segm 14, dB, dA being Element of SCM+FSA-Data-Loc , fA being Element of SCM+FSA-Data*-Loc such that
A3: ins = [K,{},<*dB,fA,dA*>] and
A4: K in {9,10} ;
ins `1_3 = K by A3, RECDEF_2:def 1;
hence contradiction by A1, A4, TARSKI:def 2; :: thesis: verum

end;

A2: now

assume ins in { [K,{},<*dC,fB*>] where K is Element of Segm 14, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} } ; :: thesis: contradiction
then consider K being Element of Segm 14, dC being Element of SCM+FSA-Data-Loc , fB being Element of SCM+FSA-Data*-Loc such that
A3: ins = [K,{},<*dC,fB*>] and
A4: K in {11,12} ;
( K = 11 or K = 12 ) by A4, TARSKI:def 2;
hence contradiction by A1, A3, RECDEF_2:def 1; :: thesis: verum

end;

not ins in SCM-Instr by A1, AMI_5:36;
then not ins in SCM-Instr \/ { [J,{},<*dA,fA,dB*>] where J is Element of Segm 14, dA, dB is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : J in {9,10} } by B2, XBOOLE_0:def 3;
then not ins in (SCM-Instr \/ { [J,{},<*dA,fA,dB*>] where J is Element of Segm 14, dA, dB is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : J in {9,10} } ) \/ { [K,{},<*dC,fB*>] where K is Element of Segm 14, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} } by A2, XBOOLE_0:def 3;
then ins in { [13,{},<*dA*>] where dA is Element of SCM+FSA-Data-Loc : verum } by XBOOLE_0:def 3;
then consider dA being Element of SCM+FSA-Data-Loc such that
A5: ins = [13,{},<*dA*>] ;
reconsider b = dA as Int-Location by Def4;
take b ; :: thesis: ins = b :==1
thus ins = b :==1 by A5; :: thesis: verum