let s1, s2 be State of S; ( ex k being Nat st
( s1 = Comput (p,s,k) & CurInstr (p,s1) = halt S ) & ex k being Nat st
( s2 = Comput (p,s,k) & CurInstr (p,s2) = halt S ) implies s1 = s2 )
given k1 being Nat such that A2:
( s1 = Comput (p,s,k1) & CurInstr (p,s1) = halt S )
; ( for k being Nat holds
( not s2 = Comput (p,s,k) or not CurInstr (p,s2) = halt S ) or s1 = s2 )
given k2 being Nat such that A3:
( s2 = Comput (p,s,k2) & CurInstr (p,s2) = halt S )
; s1 = s2
( k1 <= k2 or k2 <= k1 )
;
hence
s1 = s2
by A2, A3, Th5; verum