let il be Element of NAT ; NIC ((halt SCM+FSA),il) = {il}
now let x be
set ;
( x in {il} iff x in { (IC (Exec ((halt SCM+FSA),s))) where s is Element of product the Object-Kind of SCM+FSA : IC s = il } )A1:
now reconsider il1 =
il as
Element of
ObjectKind (IC ) by COMPOS_1:def 6;
reconsider I =
halt SCM+FSA as
Element of the
Object-Kind of
SCM+FSA . il by COMPOS_1:def 8;
reconsider n =
il1 as
Element of
NAT ;
set t = the
State of
SCM+FSA;
assume A2:
x = il
;
x in { (IC (Exec ((halt SCM+FSA),s))) where s is Element of product the Object-Kind of SCM+FSA : IC s = il } reconsider p = (
(IC ),
il)
--> (
il1,
I) as
PartState of
SCM+FSA by COMPOS_1:37;
reconsider u = the
State of
SCM+FSA +* p as
Element of
product the
Object-Kind of
SCM+FSA by PBOOLE:155;
A3:
IC u = n
by EXTPRO_1:26;
dom (((IC ),il) --> (il1,I)) = {(IC ),il}
by FUNCT_4:65;
then A4:
IC in dom (((IC ),il) --> (il1,I))
by TARSKI:def 2;
IC (Exec ((halt SCM+FSA),u)) =
u . (IC )
by EXTPRO_1:def 3
.=
(((IC ),il) --> (il1,I)) . (IC )
by A4, FUNCT_4:14
.=
il
by COMPOS_1:3, FUNCT_4:66
;
hence
x in { (IC (Exec ((halt SCM+FSA),s))) where s is Element of product the Object-Kind of SCM+FSA : IC s = il }
by A2, A3;
verum end; hence
(
x in {il} iff
x in { (IC (Exec ((halt SCM+FSA),s))) where s is Element of product the Object-Kind of SCM+FSA : IC s = il } )
by A1, TARSKI:def 1;
verum end;
hence
NIC ((halt SCM+FSA),il) = {il}
by TARSKI:2; verum