B: 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 Z1: (Macro i) . f = halt S ; :: thesis: ( not f in dom (Macro i) or f = LastLoc (Macro i) )
assume Z2: 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 Z1, COMPOS_0:def 12; :: thesis: verum

end;

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

end;