let il, k be Nat; :: thesis: NIC ((),il) = {k}
now :: thesis: for x being object holds
( x in {k} iff x in { (IC (Exec ((),s))) where s is Element of product : IC s = il } )
let x be object ; :: thesis: ( x in {k} iff x in { (IC (Exec ((),s))) where s is Element of product : IC s = il } )
A1: now :: thesis: ( x = k implies x in { (IC (Exec ((),s))) where s is Element of product : IC s = il } )
il in NAT by ORDINAL1:def 12;
then reconsider il1 = il as Element of Values () 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 ((),s))) where s is Element of product : IC s = il }
reconsider n = il as Element of NAT by ORDINAL1:def 12;
reconsider u = the State of SCM +* ((),il1) as Element of product by CARD_3:107;
reconsider P = the Instruction-Sequence of SCM +* (il,()) 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 ;
hence x in { (IC (Exec ((),s))) where s is Element of product : IC s = il } by A2, A4, A3, A5; :: thesis: verum
end;
now :: thesis: ( x in { (IC (Exec ((),s))) where s is Element of product : IC s = il } implies x = k )
assume x in { (IC (Exec ((),s))) where s is Element of product : IC s = il } ; :: thesis: x = k
then ex s being Element of product st
( x = IC (Exec ((),s)) & IC s = il ) ;
hence x = k by AMI_3:7; :: thesis: verum
end;
hence ( x in {k} iff x in { (IC (Exec ((),s))) where s is Element of product : IC s = il } ) by ; :: thesis: verum
end;
hence NIC ((),il) = {k} by TARSKI:2; :: thesis: verum