let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for P being the Instructions of b₁ -valued ManySortedSet of NAT
for s being State of S
for k being Element of NAT st P halts_on s holds
( Result P,s = Comput P,s,k iff P halts_at IC (Comput P,s,k) )
let S be non empty stored-program halting IC-Ins-separated steady-programmed definite AMI-Struct of N; :: thesis: for P being the Instructions of S -valued ManySortedSet of NAT
for s being State of S
for k being Element of NAT st P halts_on s holds
( Result P,s = Comput P,s,k iff P halts_at IC (Comput P,s,k) )
let P be the Instructions of S -valued ManySortedSet of NAT ; :: thesis: for s being State of S
for k being Element of NAT st P halts_on s holds
( Result P,s = Comput P,s,k iff P halts_at IC (Comput P,s,k) )
let s be State of S; :: thesis: for k being Element of NAT st P halts_on s holds
( Result P,s = Comput P,s,k iff P halts_at IC (Comput P,s,k) )
let k be Element of NAT ; :: thesis: ( P halts_on s implies ( Result P,s = Comput P,s,k iff P halts_at IC (Comput P,s,k) ) )
assume A1: P halts_on s ; :: thesis: ( Result P,s = Comput P,s,k iff P halts_at IC (Comput P,s,k) )
X: dom P = NAT by PARTFUN1:def 4;

hereby :: thesis: ( P halts_at IC (Comput P,s,k) implies Result P,s = Comput P,s,k )

assume Result P,s = Comput P,s,k ; :: thesis: P halts_at IC (Comput P,s,k)
then ex i being Element of NAT st
( Comput P,s,k = Comput P,s,i & CurInstr P,(Comput P,s,k) = halt S ) by A1, Def22;
then CurInstr P,(Comput P,s,k) = halt S ;
then P /. (IC (Comput P,s,k)) = halt S ;
then P . (IC (Comput P,s,k)) = halt S by X, PARTFUN1:def 8;
hence P halts_at IC (Comput P,s,k) by Def45; :: thesis: verum

end;

assume P . (IC (Comput P,s,k)) = halt S ; :: according to AMI_1:def 45 :: thesis: Result P,s = Comput P,s,k
then P /. (IC (Comput P,s,k)) = halt S by X, PARTFUN1:def 8;
then CurInstr P,(Comput P,s,k) = halt S ;
hence Result P,s = Comput P,s,k by A1, Def22; :: thesis: verum