consider k being Nat such that
IC (Comput (p,s,k)) in dom p and
A4: CurInstr (p,(Comput (p,s,k))) = halt S by A1, Def7;
k in NAT by ORDINAL1:def 12;
hence ex b₁ being State of S ex k being Element of NAT st
( b₁ = Comput (p,s,k) & CurInstr (p,b₁) = halt S ) by A4; :: thesis: verum