let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis:
let s1, s2 be State of SCM+FSA; :: thesis:
let I be Program of SCM+FSA; :: thesis:
let a be Int-Location ; :: thesis:
assume A2: not I refers a ; :: thesis:
set S2 = Initialize s2;
set Q2 = P2 +* I;
set S1 = Initialize s1;
set Q1 = P1 +* I;
assume A3: for b being Int-Location st a <> b holds
s1 . b = s2 . b ; :: thesis:
assume A4: for f being FinSeq-Location holds s1 . f = s2 . f ; :: thesis:
assume that
A5: I is_closed_on s1,P1 and
A6: I is_halting_on s1,P1 ; :: thesis:

A7: now

let k be Element of NAT ; :: thesis:
IC (Comput ((P1 +* I),(Initialize s1),k)) in dom I by A5, SCMFSA7B:def 6;
hence IC (Comput ((P2 +* I),(Initialize s2),k)) in dom I by A2, Th38, A5, A4, A3; :: thesis:

end;

P1 +* I halts_on Initialize s1 by A6, SCMFSA7B:def 7;
then consider n being Element of NAT such that
A8: CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),n))) = halt SCM+FSA by EXTPRO_1:29;
CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),n))) = halt SCM+FSA by A2, A8, Th38, A5, A4, A3;
then P2 +* I halts_on Initialize s2 by EXTPRO_1:29;
hence ( I is_closed_on s2,P2 & I is_halting_on s2,P2 ) by A7, SCMFSA7B:def 6, SCMFSA7B:def 7; :: thesis: