let il be Element of NAT ; NIC (halt SCM+FSA ),il = {il}
now let x be
set ;
( x in {il} iff x in { (IC (Following (ProgramPart s),s)) where s is Element of product the Object-Kind of SCM+FSA : ( IC s = il & (ProgramPart s) /. il = halt SCM+FSA ) } )A1:
now reconsider il1 =
il as
Element of
ObjectKind (IC SCM+FSA ) by AMI_1:def 11;
reconsider I =
halt SCM+FSA as
Element of the
Object-Kind of
SCM+FSA . il by AMI_1:def 14;
reconsider n =
il1 as
Element of
NAT ;
consider t being
State of
SCM+FSA ;
assume A2:
x = il
;
x in { (IC (Following (ProgramPart s),s)) where s is Element of product the Object-Kind of SCM+FSA : ( IC s = il & (ProgramPart s) /. il = halt SCM+FSA ) } reconsider p =
(IC SCM+FSA ),
il --> il1,
I as
PartState of
SCM+FSA by AMI_1:149;
reconsider u =
t +* p as
Element of
product the
Object-Kind of
SCM+FSA by PBOOLE:155;
A3:
IC u = n
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;
X:
(ProgramPart u) /. il = u . il
by AMI_1:150;
A5:
u . n = halt SCM+FSA
by AMI_1:129;
then IC (Following (ProgramPart u),u) =
u . (IC SCM+FSA )
by A3, AMI_1:def 8, X
.=
((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 (ProgramPart s),s)) where s is Element of product the Object-Kind of SCM+FSA : ( IC s = il & (ProgramPart s) /. il = halt SCM+FSA ) }
by A2, A5, A3, X;
verum end; hence
(
x in {il} iff
x in { (IC (Following (ProgramPart s),s)) where s is Element of product the Object-Kind of SCM+FSA : ( IC s = il & (ProgramPart s) /. il = halt SCM+FSA ) } )
by A1, TARSKI:def 1;
verum end;
hence
NIC (halt SCM+FSA ),il = {il}
by TARSKI:2; verum