let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for P being the Instructions of b₁ -valued ManySortedSet of NAT
for s being State of S st ex k being Element of NAT st P . (IC (Comput P,s,k)) = halt S holds
for i being Element of NAT holds Result P,s = Result P,(Comput P,s,i)
let S be non empty stored-program IC-Ins-separated definite halting AMI-Struct of N; :: thesis: for P being the Instructions of S -valued ManySortedSet of NAT
for s being State of S st ex k being Element of NAT st P . (IC (Comput P,s,k)) = halt S holds
for i being Element of NAT holds Result P,s = Result P,(Comput P,s,i)
let P be the Instructions of S -valued ManySortedSet of NAT ; :: thesis: for s being State of S st ex k being Element of NAT st P . (IC (Comput P,s,k)) = halt S holds
for i being Element of NAT holds Result P,s = Result P,(Comput P,s,i)
let s be State of S; :: thesis: ( ex k being Element of NAT st P . (IC (Comput P,s,k)) = halt S implies for i being Element of NAT holds Result P,s = Result P,(Comput P,s,i) )
given k being Element of NAT such that A1: P . (IC (Comput P,s,k)) = halt S ; :: thesis: for i being Element of NAT holds Result P,s = Result P,(Comput P,s,i)
let i be Element of NAT ; :: thesis: Result P,s = Result P,(Comput P,s,i)
XX: dom P = NAT by PARTFUN1:def 4;
set s9 = Comput P,s,k;
IC (Comput P,s,k) in dom P by XX;
then Y: P /. (IC (Comput P,s,k)) = P . (IC (Comput P,s,k)) by PARTFUN1:def 8;
A2: CurInstr P,(Comput P,s,k) = halt S by A1, Y;

now

per cases ( i <= k or i >= k ) ;

suppose i <= k ; :: thesis: Result P,s = Result P,(Comput P,s,i)

then consider j being Nat such that
A3: k = i + j by NAT_1:10;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
A4: Comput P,s,k = Comput P,(Comput P,s,i),j by A3, Th51;
CurInstr P,(Comput P,s,k) = halt S by A2;
then A5: P halts_on Comput P,s,i by A4, Def20, XX;
thus Result P,s = Comput P,s,k by A1, Th56
.= Result P,(Comput P,s,i) by A2, A4, A5, Def22 ; :: thesis: verum

end;

suppose A6: i >= k ; :: thesis: Result P,s = Result P,(Comput P,s,i)

A7: Comput P,(Comput P,s,k),0 = Comput P,s,k by Th13;
A8: Comput P,s,i = Comput P,s,k by A2, A6, Th52;
X: IC (Comput P,(Comput P,s,k),0 ) in dom P by XX;
CurInstr P,(Comput P,(Comput P,s,k),0 ) = halt S by A2, A7;
then A9: P halts_on Comput P,s,i by Def20, X, A8;
thus Result P,s = Comput P,s,k by A1, Th56
.= Result P,(Comput P,s,i) by A2, A8, A7, A9, Def22 ; :: thesis: verum

end;

end;

end;

hence Result P,s = Result P,(Comput P,s,i) ; :: thesis: verum