halt S in rng P by COMPOS_1:def 3;
then consider i being set such that
W1: i in dom P and
W2: P . i = halt S by FUNCT_1:def 3;
dom P c= NAT by RELAT_1:def 18;
then reconsider i = i as Element of NAT by W1;
take p = Start-At (i,S); :: thesis: ( p is P -autonomic & p is P -halted & not p is empty )
i .--> (halt S) c= P by W1, W2, FUNCT_4:85;
hence ( p is P -autonomic & p is P -halted & not p is empty ) by Th11, Th13; :: thesis: verum