halt S in rng P by COMPOS_1:def 7;
then consider x being set such that
W1: x in dom P and
W2: P . x = halt S by FUNCT_1:def 5;
dom P c= NAT by RELAT_1:def 18;
then reconsider m = x as Element of NAT by W1;
[m,(halt S)] in P by W1, W2, FUNCT_1:def 4;
then {[m,(halt S)]} c= P by ZFMISC_1:37;
then A1: m .--> (halt S) c= P by FUNCT_4:87;
take d = Start-At (m,S); :: thesis: ( d +* P is autonomic & d +* P is halting )
thus d +* P is autonomic by A1, Th12; :: thesis: d +* P is halting
thus d +* P is halting by A1, Th10; :: thesis: verum