let F be non empty preProgram of S; :: thesis: ( F is trivial implies F is unique-halt )
assume A1: F is trivial ; :: thesis: F is unique-halt
let f be Nat; :: according to COMPOS_1:def 15 :: thesis: ( F . f = halt S & f in dom F implies f = LastLoc F )
assume that
F . f = halt S and
A2: f in dom F ; :: thesis: f = LastLoc F
consider x being object such that
A3: F = {x} by A1, ZFMISC_1:131;
x in F by A3, TARSKI:def 1;
then consider a, b being object such that
A4: [a,b] = x by RELAT_1:def 1;
A5: LastLoc F in dom F by VALUED_1:30;
A6: dom F = {a} by A3, A4, RELAT_1:9;
hence f = a by A2, TARSKI:def 1
.= LastLoc F by A5, A6, TARSKI:def 1 ;
:: thesis: verum