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

.= 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)

end;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

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

then (Macro i) . f = i by COMPOS_1:58;

hence contradiction by A2, COMPOS_0:def 12; :: thesis: verum

end;then (Macro i) . f = i by COMPOS_1:58;

hence contradiction by A2, COMPOS_0:def 12; :: thesis: verum