let s1, s2 be State of SCM+FSA; :: thesis:
let P1, P2 be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis:
let I be parahalting Program of SCM+FSA; :: thesis:
assume that
A1: I c= P1 and
A2: I c= P2 and
A3: Start-At (0,SCM+FSA) c= s1 and
A4: Start-At (0,SCM+FSA) c= s2 and
A5: NPP s1 = NPP s2 ; :: thesis:

hereby :: thesis:

let k be Element of NAT ; :: thesis:
A6: IC (Comput (P1,s1,k)) in dom I by A3, Def2, A1;
A7: IC (Comput (P2,s2,k)) in dom I by A4, Def2, A2;
for m being Element of NAT st m < k holds
IC (Comput (P2,s2,m)) in dom I by A4, Def2, A2;
hence NPP (Comput (P1,s1,k)) = NPP (Comput (P2,s2,k)) by A5, A1, A2, AMISTD_2:66; :: thesis:
then A8: 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
.= I . (IC (Comput (P2,s2,k))) by A7, A2, GRFUNC_1:8
.= P1 . (IC (Comput (P1,s1,k))) by A8, A6, A1, GRFUNC_1:8
.= CurInstr (P1,(Comput (P1,s1,k))) by PBOOLE:158 ; :: thesis:

end;