let ins be Instruction of SCM ; :: thesis: ( InsCode ins = 7 implies ex loc being Instruction-Location of SCM ex da being Data-Location st ins = da =0_goto loc )
assume A1: InsCode ins = 7 ; :: thesis: ex loc being Instruction-Location of SCM ex da being Data-Location st ins = da =0_goto loc
A2: not ins in {[SCM-Halt ,{} ]} by A1, Th37, AMI_3:71, TARSKI:def 1;

A3: now

assume ins in { [J,<*a*>] where J is Element of Segm 9, a is Element of NAT : J = 6 } ; :: thesis: contradiction
then consider J being Element of Segm 9, a being Element of NAT such that
A4: ins = [J,<*a*>] and
A5: J = 6 ;
thus contradiction by A1, A4, A5, MCART_1:7; :: thesis: verum

end;

A6: now

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

end;

A9: not ins in {[SCM-Halt ,{} ]} \/ { [J,<*a*>] where J is Element of Segm 9, a is Element of NAT : J = 6 } by A2, A3, XBOOLE_0:def 3;
ins in ({[SCM-Halt ,{} ]} \/ { [J,<*a*>] where J is Element of Segm 9, a is Element of NAT : J = 6 } ) \/ { [K,<*a1,b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } by A6, XBOOLE_0:def 3;
then ins in { [K,<*a1,b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } by A9, XBOOLE_0:def 3;
then consider K being Element of Segm 9, a1 being Element of NAT , b1 being Element of SCM-Data-Loc such that
A10: ins = [K,<*a1,b1*>] and
K in {7,8} ;
reconsider loc = a1 @ as Instruction-Location of SCM ;
reconsider da = b1 @ as Data-Location ;
take loc ; :: thesis: ex da being Data-Location st ins = da =0_goto loc
take da ; :: thesis: ins = da =0_goto loc
thus ins = da =0_goto loc by A1, A10, MCART_1:7; :: thesis: verum