let il be Element of NAT ; :: thesis: for k being natural number holds NIC (SCM-goto k),il = {k}
let k be natural number ; :: thesis: NIC (SCM-goto k),il = {k}

now

let x be set ; :: thesis: ( x in {k} iff x in { (IC (Following (ProgramPart s),s)) where s is Element of product the Object-Kind of SCM : ( IC s = il & (ProgramPart s) /. il = SCM-goto k ) } )

A1: now

reconsider il1 = il as Element of ObjectKind (IC SCM ) by COMPOS_1:def 6;
reconsider I = SCM-goto k as Element of the Object-Kind of SCM . il by COMPOS_1:def 8;
consider t being State of SCM ;
assume A2: x = k ; :: thesis: x in { (IC (Following (ProgramPart s),s)) where s is Element of product the Object-Kind of SCM : ( IC s = il & (ProgramPart s) /. il = SCM-goto k ) }
reconsider n = il as Element of NAT ;
reconsider p = (IC SCM ),il --> il1,I as PartState of SCM by COMPOS_1:37;
reconsider u = t +* p as Element of product the Object-Kind of SCM by PBOOLE:155;
X: (ProgramPart u) /. il = u . il by COMPOS_1:38;
A3: ( IC u = n & u . n = SCM-goto k ) by AMI_1:129;
then IC (Following (ProgramPart u),u) = k by X, AMI_3:13;
hence x in { (IC (Following (ProgramPart s),s)) where s is Element of product the Object-Kind of SCM : ( IC s = il & (ProgramPart s) /. il = SCM-goto k ) } by A2, A3, X; :: thesis: verum

end;

now

assume x in { (IC (Following (ProgramPart s),s)) where s is Element of product the Object-Kind of SCM : ( IC s = il & (ProgramPart s) /. il = SCM-goto k ) } ; :: thesis: x = k
then ex s being Element of product the Object-Kind of SCM st
( x = IC (Following (ProgramPart s),s) & IC s = il & (ProgramPart s) /. il = SCM-goto k ) ;
hence x = k by AMI_3:13; :: thesis: verum

end;

hence ( x in {k} iff x in { (IC (Following (ProgramPart s),s)) where s is Element of product the Object-Kind of SCM : ( IC s = il & (ProgramPart s) /. il = SCM-goto k ) } ) by A1, TARSKI:def 1; :: thesis: verum

end;

hence NIC (SCM-goto k),il = {k} by TARSKI:2; :: thesis: verum