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

A2: now

assume 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} } ; :: thesis: contradiction
then consider K being Element of Segm 13, 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;

( ins in SCM-Instr \/ { [L,{} ,<*dB,fA,dA*>] where L is Element of Segm 13, dB, dA 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;
then ( ins in SCM-Instr or ins in { [L,{} ,<*dB,fA,dA*>] where L is Element of Segm 13, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } ) by A2, XBOOLE_0:def 3;
then consider L being Element of Segm 13, dB, dA being Element of SCM+FSA-Data-Loc , fA being Element of SCM+FSA-Data*-Loc such that
A5: ins = [L,{} ,<*dB,fA,dA*>] and
L in {9,10} by A1, AMI_5:36;
reconsider f = fA as FinSeq-Location by Def5;
reconsider c = dB, b = dA as Int-Location by Def4;
take b ; :: thesis: ex b being Int-Location ex fa being FinSeq-Location st ins = fa,b := b
take c ; :: thesis: ex fa being FinSeq-Location st ins = fa,b := c
take f ; :: thesis: ins = f,b := c
thus ins = f,b := c by A1, A5, RECDEF_2:def 1; :: thesis: verum