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

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