let ins be Instruction of SCM+FSA; :: thesis: ( InsCode ins = 12 implies ex a being Int-Location ex fa being FinSeq-Location st ins = fa :=<0,...,0> a )
assume A1: InsCode ins = 12 ; :: thesis: ex a being Int-Location ex fa being FinSeq-Location st ins = fa :=<0,...,0> a

A2: now :: thesis: not ins in { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dA, dB is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} }

assume ins in { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dA, dB 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 13, dA, dB 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;
hence contradiction by A1, A4, TARSKI:def 2; :: thesis: verum

end;

A5: ( ins in SCM-Instr \/ { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dA, dB is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } or ins in { [K,{},<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} } ) by XBOOLE_0:def 3;
not ins in SCM-Instr by A1, AMI_5:5;
then consider K being Element of Segm 13, dB being Element of SCM+FSA-Data-Loc , fA being Element of SCM+FSA-Data*-Loc such that
A6: ins = [K,{},<*dB,fA*>] and
K in {11,12} by A5, A2, XBOOLE_0:def 3;
reconsider f = fA as FinSeq-Location by Def3;
reconsider c = dB as Int-Location by AMI_2:def 16;
take c ; :: thesis: ex fa being FinSeq-Location st ins = fa :=<0,...,0> c
take f ; :: thesis: ins = f :=<0,...,0> c
thus ins = f :=<0,...,0> c by A1, A6; :: thesis: verum