set P = (IC (SCM R)),0 --> 0 ,(halt (SCM R));
il. (SCM R),0 = 0 by SCMRING3:66;
then (IC (SCM R)),0 --> 0 ,(halt (SCM R)) = (Start-At (il. (SCM R),0 ),(SCM R)) +* ((il. (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 AMI_1:48; :: thesis: verum

end;

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