A1: LastLoc (Macro i) = (card (Macro i)) -' 1 by AFINSQ_1:70
.= 2 -' 1 by COMPOS_1:56
.= 2 - 1 by XREAL_1:233
.= 1 ;
hence (Macro i) . (LastLoc (Macro i)) = halt S by COMPOS_1:59; :: according to COMPOS_1:def 14 :: thesis: Macro i is unique-halt
thus Macro i is unique-halt :: thesis: verum

proof

let f be Nat; :: according to COMPOS_1:def 15 :: thesis: ( not (Macro i) . f = halt S or not f in dom (Macro i) or f = LastLoc (Macro i) )
assume A2: (Macro i) . f = halt S ; :: thesis: ( not f in dom (Macro i) or f = LastLoc (Macro i) )
assume A3: f in dom (Macro i) ; :: thesis: f = LastLoc (Macro i)

now :: thesis: not f = 0

assume f = 0 ; :: thesis: contradiction
then (Macro i) . f = i by COMPOS_1:58;
hence contradiction by A2, COMPOS_0:def 12; :: thesis: verum

end;

hence f = LastLoc (Macro i) by A3, A1, COMPOS_1:60; :: thesis: verum

end;