let p be non empty preProgram of S; :: thesis: ( p is halt-free implies p is unique-halt )
assume Z: p is halt-free ; :: thesis: p is unique-halt
let k be Nat; :: according to COMPOS_1:def 9 :: thesis: ( p . k = halt S & k in dom p implies k = LastLoc p )
assume that
Z1: p . k = halt S and
Z2: k in dom p ; :: thesis: k = LastLoc p
p . k <> halt S by Def25, Z2, Z;
hence k = LastLoc p by Z1; :: thesis: verum