let R be good Ring; :: thesis:
let il be Element of NAT ; :: thesis:

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

end;

assume x in { (IC (Exec ((halt (SCM R)),s))) where s is Element of product the Object-Kind of (SCM R) : IC s = il } ; :: thesis:
then consider s being Element of product the Object-Kind of (SCM R) such that
A8: ( x = IC (Exec ((halt (SCM R)),s)) & IC s = il ) ;
thus x = il by A8, EXTPRO_1:def 3; :: thesis:

end;

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

end;