let F be NAT -defined non empty FinPartState of ; :: thesis: ( F is trivial implies F is unique-halt )
assume A1: F is trivial ; :: thesis: F is unique-halt
let f be Element of NAT ; :: according to COMPOS_1:def 26 :: thesis: ( not F . f = halt S or not f in proj1 F or f = LastLoc F )
assume that
F . f = halt S and
A2: f in dom F ; :: thesis: f = LastLoc F
consider x being set such that
A3: F = {x} by A1, REALSET1:def 4;
x in F by A3, TARSKI:def 1;
then consider a, b being set such that
A4: [a,b] = x by RELAT_1:def 1;
A5: LastLoc F in dom F by VALUED_1:31;
A6: dom F = {a} by A3, A4, RELAT_1:23;
hence f = a by A2, TARSKI:def 1
.= LastLoc F by A5, A6, TARSKI:def 1 ;
:: thesis: verum