set P = (IC SCM+FSA ),0 --> 0 ,(halt SCM+FSA );
(IC SCM+FSA ),0 --> 0 ,(halt SCM+FSA ) = (Start-At 0 ,SCM+FSA ) +* (0 .--> (halt SCM+FSA )) by FUNCT_4:def 4;
then reconsider P = (IC SCM+FSA ),0 --> 0 ,(halt SCM+FSA ) as FinPartState of SCM+FSA ;
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

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

end;

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