set P = (IC (SCM R)),0 --> 0 ,(halt (SCM R));
(IC (SCM R)),0 --> 0 ,(halt (SCM R)) = (Start-At 0 ,(SCM R)) +* (0 .--> (halt (SCM R))) by FUNCT_4:def 4;
then reconsider P = (IC (SCM R)),0 --> 0 ,(halt (SCM R)) as FinPartState of (SCM R) ;
take P ; :: thesis: ( P is autonomic & not P is NAT -defined )
thus P is autonomic by AMI_1:67; :: thesis: not P is NAT -defined

now

dom P = {(IC (SCM R)),0 } by FUNCT_4:65;
then A1: IC (SCM R) in dom P by TARSKI:def 2;
assume dom P c= NAT ; :: thesis: contradiction
then reconsider l = IC (SCM R) as Element of NAT by A1;
l = IC (SCM R) ;
hence contradiction by COMPOS_1:3; :: thesis: verum

end;

hence not P is NAT -defined by RELAT_1:def 18; :: thesis: verum