halt S in rng P by COMPOS_1:def 11;
then consider x being object such that
A1: x in dom P and
A2: P . x = halt S by FUNCT_1:def 3;
dom P c= NAT by RELAT_1:def 18;
then reconsider m = x as Nat by A1;
[m,(halt S)] in P by A1, A2, FUNCT_1:def 2;
then {[m,(halt S)]} c= P by ZFMISC_1:31;
then A3: m .--> (halt S) c= P by FUNCT_4:82;
take d = Start-At (m,S); :: thesis: ( d is P -autonomic & d is P -halted )
thus d is P -autonomic by A3, Th12; :: thesis: d is P -halted
thus d is P -halted by A3, Th10; :: thesis: verum