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

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