halt S in rng P by COMPOS_1:def 11;
then consider i being object such that
A1: i in dom P and
A2: P . i = halt S by FUNCT_1:def 3;
dom P c= NAT by RELAT_1:def 18;
then reconsider i = i as Nat by A1;
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 A1, A2, FUNCT_4:85;
hence ( p is P -autonomic & p is P -halted & not p is empty ) by Th10, Th12; :: thesis: verum