let il be Instruction-Location of SCM+FSA ; :: thesis: NIC (halt SCM+FSA ),il = {il}

now

let x be set ; :: thesis: ( x in {il} iff x in { (IC (Following s)) where s is State of : ( IC s = il & s . il = halt SCM+FSA ) } )

A1: now

il in NAT by AMI_1:def 4;
then reconsider il1 = il as Element of ObjectKind (IC SCM+FSA ) by AMI_1:def 11;
reconsider I = halt SCM+FSA as Element of ObjectKind il by AMI_1:def 14;
consider t being State of ;
assume A2: x = il ; :: thesis: x in { (IC (Following s)) where s is State of : ( IC s = il & s . il = halt SCM+FSA ) }
set u = t +* ((IC SCM+FSA ),il --> il1,I);
A3: IC (t +* ((IC SCM+FSA ),il --> il1,I)) = il by AMI_1:129;
dom ((IC SCM+FSA ),il --> il1,I) = {(IC SCM+FSA ),il} by FUNCT_4:65;
then A4: IC SCM+FSA in dom ((IC SCM+FSA ),il --> il1,I) by TARSKI:def 2;
A5: (t +* ((IC SCM+FSA ),il --> il1,I)) . il = halt SCM+FSA by AMI_1:129;
then IC (Following (t +* ((IC SCM+FSA ),il --> il1,I))) = (t +* ((IC SCM+FSA ),il --> il1,I)) . (IC SCM+FSA ) by A3, AMI_1:def 8
.= ((IC SCM+FSA ),il --> il1,I) . (IC SCM+FSA ) by A4, FUNCT_4:14
.= il by AMI_1:48, FUNCT_4:66 ;
hence x in { (IC (Following s)) where s is State of : ( IC s = il & s . il = halt SCM+FSA ) } by A2, A5, A3; :: thesis: verum

end;

now

assume x in { (IC (Following s)) where s is State of : ( IC s = il & s . il = halt SCM+FSA ) } ; :: thesis: x = il
then ex s being State of st
( x = IC (Following s) & IC s = il & s . il = halt SCM+FSA ) ;
hence x = il by AMI_1:def 8; :: thesis: verum

end;

hence ( x in {il} iff x in { (IC (Following s)) where s is State of : ( IC s = il & s . il = halt SCM+FSA ) } ) by A1, TARSKI:def 1; :: thesis: verum

end;

hence NIC (halt SCM+FSA ),il = {il} by TARSKI:2; :: thesis: verum