let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I being InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= P1 & I c= P2 holds
for k being Element of NAT holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )
let s be State of SCM+FSA; :: thesis: for I being InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= P1 & I c= P2 holds
for k being Element of NAT holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )
let I be InitHalting Program of SCM+FSA; :: thesis: ( Initialize ((intloc 0) .--> 1) c= s & I c= P1 & I c= P2 implies for k being Element of NAT holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) ) )
assume that
A1: Initialize ((intloc 0) .--> 1) c= s and
A2: I c= P1 and
A3: I c= P2 ; :: thesis: for k being Element of NAT holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )

hereby :: thesis: verum

let k be Element of NAT ; :: thesis: ( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P2,(Comput (P2,s,k))) = CurInstr (P1,(Comput (P1,s,k))) )
A4: IC (Comput (P1,s,k)) in dom I by A1, A2, SCM_HALT:def 1;
A5: IC (Comput (P2,s,k)) in dom I by A1, A3, SCM_HALT:def 1;
for m being Element of NAT st m < k holds
IC (Comput (P2,s,m)) in dom I by A1, A3, SCM_HALT:def 1;
hence Comput (P1,s,k) = Comput (P2,s,k) by A2, A3, AMISTD_2:10; :: thesis: CurInstr (P2,(Comput (P2,s,k))) = CurInstr (P1,(Comput (P1,s,k)))
then A6: IC (Comput (P1,s,k)) = IC (Comput (P2,s,k)) ;
thus CurInstr (P2,(Comput (P2,s,k))) = P2 . (IC (Comput (P2,s,k))) by PBOOLE:143
.= I . (IC (Comput (P2,s,k))) by A5, A3, GRFUNC_1:2
.= P1 . (IC (Comput (P1,s,k))) by A6, A4, A2, GRFUNC_1:2
.= CurInstr (P1,(Comput (P1,s,k))) by PBOOLE:143 ; :: thesis: verum

end;