let R be good Ring; :: thesis: for i1, il being Element of NAT holds NIC ((goto (i1,R)),il) = {i1}
let i1, il be Element of NAT ; :: thesis: NIC ((goto (i1,R)),il) = {i1}

now

let x be set ; :: thesis: ( x in {i1} iff x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product the Object-Kind of (SCM R) : IC s = il } )

A1: now

reconsider il1 = il as Element of ObjectKind (IC (SCM R)) by COMPOS_1:def 6;
reconsider I = goto (i1,R) as Element of the Object-Kind of (SCM R) . il by COMPOS_1:def 8;
consider t being State of (SCM R);
assume A2: x = i1 ; :: thesis: x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product the Object-Kind of (SCM R) : IC s = il }
reconsider p = ((IC (SCM R)),il) --> (il1,I) as PartState of (SCM R) by COMPOS_1:37;
reconsider u = t +* p as Element of product the Object-Kind of (SCM R) by PBOOLE:155;
A3: dom (((IC (SCM R)),il) --> (il1,I)) = {(IC (SCM R)),il} by FUNCT_4:65;
then il in dom (((IC (SCM R)),il) --> (il1,I)) by TARSKI:def 2;
then A4: u . il = (((IC (SCM R)),il) --> (il1,I)) . il by FUNCT_4:14
.= goto (i1,R) by FUNCT_4:66 ;
X: (ProgramPart u) /. il = u . il by COMPOS_1:38;
IC (SCM R) in dom (((IC (SCM R)),il) --> (il1,I)) by A3, TARSKI:def 2;
then A5: IC u = (((IC (SCM R)),il) --> (il1,I)) . (IC (SCM R)) by FUNCT_4:14
.= il by COMPOS_1:3, FUNCT_4:66 ;
then IC (Following ((ProgramPart u),u)) = i1 by A4, X, SCMRING2:17;
hence x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product the Object-Kind of (SCM R) : IC s = il } by A2, A5, A4, X; :: thesis: verum

end;

now

assume x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product the Object-Kind of (SCM R) : IC s = il } ; :: thesis: x = i1
then ex s being Element of product the Object-Kind of (SCM R) st
( x = IC (Exec ((goto (i1,R)),s)) & IC s = il ) ;
hence x = i1 by SCMRING2:17; :: thesis: verum

end;

hence ( x in {i1} iff x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product the Object-Kind of (SCM R) : IC s = il } ) by A1, TARSKI:def 1; :: thesis: verum

end;

hence NIC ((goto (i1,R)),il) = {i1} by TARSKI:2; :: thesis: verum