let ins be Instruction of SCM; :: thesis: ( InsCode ins = 6 implies ex loc being Nat st ins = SCM-goto loc )
assume A1: InsCode ins = 6 ; :: thesis: ex loc being Nat st ins = SCM-goto loc

now :: thesis: not ins in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of Data-Locations : I in {1,2,3,4,5} }

assume ins in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of Data-Locations : I in {1,2,3,4,5} } ; :: thesis: contradiction
then consider I being Element of Segm 9, b, c being Element of Data-Locations such that
A2: ins = [I,{},<*b,c*>] and
A3: I in {1,2,3,4,5} ;
InsCode ins = I by A2;
hence contradiction by A1, A3, ENUMSET1:def 3; :: thesis: verum

end;

then A4: ins in ({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of Data-Locations : K in {7,8} } by AMI_3:27, XBOOLE_0:def 3;

now :: thesis: not ins in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of Data-Locations : K in {7,8} }

assume ins in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of Data-Locations : K in {7,8} } ; :: thesis: contradiction
then consider K being Element of Segm 9, a1 being Nat, b1 being Element of Data-Locations such that
A5: ins = [K,<*a1*>,<*b1*>] and
A6: K in {7,8} ;
InsCode ins = K by A5;
hence contradiction by A1, A6, TARSKI:def 2; :: thesis: verum

end;

then A7: ins in {[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } by A4, XBOOLE_0:def 3;
InsCode (halt SCM) = 0 by COMPOS_1:70;
then not ins in {[SCM-Halt,{},{}]} by A1, AMI_3:26, TARSKI:def 1;
then ins in { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } by A7, XBOOLE_0:def 3;
then consider J being Element of Segm 9, a being Nat such that
A8: ( ins = [J,<*a*>,{}] & J = 6 ) ;
reconsider loc = a as Nat ;
take loc ; :: thesis: ins = SCM-goto loc
thus ins = SCM-goto loc by A8; :: thesis: verum