let il, k be Nat; :: thesis: NIC ((SCM-goto k),il) = {k}

now :: thesis: for x being object holds

( x in {k} iff x in { (IC (Exec ((SCM-goto k),s))) where s is Element of product (the_Values_of SCM) : IC s = il } )

hence
NIC ((SCM-goto k),il) = {k}
by TARSKI:2; :: thesis: verum( x in {k} iff x in { (IC (Exec ((SCM-goto k),s))) where s is Element of product (the_Values_of SCM) : IC s = il } )

let x be object ; :: thesis: ( x in {k} iff x in { (IC (Exec ((SCM-goto k),s))) where s is Element of product (the_Values_of SCM) : IC s = il } )

end;A1: now :: thesis: ( x = k implies x in { (IC (Exec ((SCM-goto k),s))) where s is Element of product (the_Values_of SCM) : IC s = il } )

il in NAT
by ORDINAL1:def 12;

then reconsider il1 = il as Element of Values (IC ) by MEMSTR_0:def 6;

set I = SCM-goto k;

set t = the State of SCM;

set Q = the Instruction-Sequence of SCM;

assume A2: x = k ; :: thesis: x in { (IC (Exec ((SCM-goto k),s))) where s is Element of product (the_Values_of SCM) : IC s = il }

reconsider n = il as Element of NAT by ORDINAL1:def 12;

reconsider u = the State of SCM +* ((IC ),il1) as Element of product (the_Values_of SCM) by CARD_3:107;

reconsider P = the Instruction-Sequence of SCM +* (il,(SCM-goto k)) as Instruction-Sequence of SCM ;

reconsider ill = il as Element of NAT by ORDINAL1:def 12;

A3: P /. ill = P . ill by PBOOLE:143;

IC in dom the State of SCM by MEMSTR_0:2;

then A4: IC u = n by FUNCT_7:31;

il in NAT by ORDINAL1:def 12;

then il in dom the Instruction-Sequence of SCM by PARTFUN1:def 2;

then A5: P . n = SCM-goto k by FUNCT_7:31;

then IC (Following (P,u)) = k by A3, A4, AMI_3:7;

hence x in { (IC (Exec ((SCM-goto k),s))) where s is Element of product (the_Values_of SCM) : IC s = il } by A2, A4, A3, A5; :: thesis: verum

end;then reconsider il1 = il as Element of Values (IC ) by MEMSTR_0:def 6;

set I = SCM-goto k;

set t = the State of SCM;

set Q = the Instruction-Sequence of SCM;

assume A2: x = k ; :: thesis: x in { (IC (Exec ((SCM-goto k),s))) where s is Element of product (the_Values_of SCM) : IC s = il }

reconsider n = il as Element of NAT by ORDINAL1:def 12;

reconsider u = the State of SCM +* ((IC ),il1) as Element of product (the_Values_of SCM) by CARD_3:107;

reconsider P = the Instruction-Sequence of SCM +* (il,(SCM-goto k)) as Instruction-Sequence of SCM ;

reconsider ill = il as Element of NAT by ORDINAL1:def 12;

A3: P /. ill = P . ill by PBOOLE:143;

IC in dom the State of SCM by MEMSTR_0:2;

then A4: IC u = n by FUNCT_7:31;

il in NAT by ORDINAL1:def 12;

then il in dom the Instruction-Sequence of SCM by PARTFUN1:def 2;

then A5: P . n = SCM-goto k by FUNCT_7:31;

then IC (Following (P,u)) = k by A3, A4, AMI_3:7;

hence x in { (IC (Exec ((SCM-goto k),s))) where s is Element of product (the_Values_of SCM) : IC s = il } by A2, A4, A3, A5; :: thesis: verum

now :: thesis: ( x in { (IC (Exec ((SCM-goto k),s))) where s is Element of product (the_Values_of SCM) : IC s = il } implies x = k )

hence
( x in {k} iff x in { (IC (Exec ((SCM-goto k),s))) where s is Element of product (the_Values_of SCM) : IC s = il } )
by A1, TARSKI:def 1; :: thesis: verumassume
x in { (IC (Exec ((SCM-goto k),s))) where s is Element of product (the_Values_of SCM) : IC s = il }
; :: thesis: x = k

then ex s being Element of product (the_Values_of SCM) st

( x = IC (Exec ((SCM-goto k),s)) & IC s = il ) ;

hence x = k by AMI_3:7; :: thesis: verum

end;then ex s being Element of product (the_Values_of SCM) st

( x = IC (Exec ((SCM-goto k),s)) & IC s = il ) ;

hence x = k by AMI_3:7; :: thesis: verum