let p be non empty preProgram of S; :: thesis: ( p is halt-free implies p is unique-halt )
assume A1: p is halt-free ; :: thesis: p is unique-halt
let k be Nat; :: according to COMPOS_1:def 15 :: thesis: ( p . k = halt S & k in dom p implies k = LastLoc p )
assume that
A2: p . k = halt S and
A3: k in dom p ; :: thesis: k = LastLoc p
thus k = LastLoc p by A2, Def27, A3, A1; :: thesis: verum