let P1, P2 be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis:
let s1, s2 be 0 -started State of SCMPDS; :: thesis:
let I be parahalting Program of SCMPDS; :: thesis:
set SI = stop I;
assume that
A1: stop I c= P1 and
A2: stop I c= P2 and
A3: NPP s1 = NPP s2 ; :: thesis:

hereby :: thesis:

let k be Element of NAT ; :: thesis:
A4: IC (Comput (P1,s1,k)) in dom (stop I) by A1, SCMPDS_4:def 9;
A5: IC (Comput (P2,s2,k)) in dom (stop I) by A2, SCMPDS_4:def 9;
for m being Element of NAT st m < k holds
IC (Comput (P2,s2,m)) in dom (stop I) by A2, SCMPDS_4:def 9;
hence NPP (Comput (P1,s1,k)) = NPP (Comput (P2,s2,k)) by A3, A1, A2, SCMPDS_4:67; :: thesis:
then A6: IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) by COMPOS_1:230;
thus CurInstr (P2,(Comput (P2,s2,k))) = P2 . (IC (Comput (P2,s2,k))) by PBOOLE:158
.= (stop I) . (IC (Comput (P2,s2,k))) by A2, A5, GRFUNC_1:8
.= P1 . (IC (Comput (P1,s1,k))) by A1, A6, A4, GRFUNC_1:8
.= CurInstr (P1,(Comput (P1,s1,k))) by PBOOLE:158 ; :: thesis:

end;