let s1, s2 be State of ; :: thesis: for I being Program of st I is_closed_on s1 & DataPart s1 = DataPart s2 holds
for k being Element of NAT holds
( Computation (s1 +* (Initialized (stop I))),k, Computation (s2 +* (Initialized (stop I))),k equal_outside NAT & CurInstr (Computation (s1 +* (Initialized (stop I))),k) = CurInstr (Computation (s2 +* (Initialized (stop I))),k) )
let I be Program of ; :: thesis: ( I is_closed_on s1 & DataPart s1 = DataPart s2 implies for k being Element of NAT holds
( Computation (s1 +* (Initialized (stop I))),k, Computation (s2 +* (Initialized (stop I))),k equal_outside NAT & CurInstr (Computation (s1 +* (Initialized (stop I))),k) = CurInstr (Computation (s2 +* (Initialized (stop I))),k) ) )
assume A1: I is_closed_on s1 ; :: thesis: ( not DataPart s1 = DataPart s2 or for k being Element of NAT holds
( Computation (s1 +* (Initialized (stop I))),k, Computation (s2 +* (Initialized (stop I))),k equal_outside NAT & CurInstr (Computation (s1 +* (Initialized (stop I))),k) = CurInstr (Computation (s2 +* (Initialized (stop I))),k) ) )
set pI = stop I;
set IsI = Initialized (stop I);
set ss1 = s1 +* (Initialized (stop I));
set ss2 = s2 +* (Initialized (stop I));
A2: stop I c= Initialized (stop I) by SCMPDS_4:9;
Initialized (stop I) c= s2 +* (Initialized (stop I)) by FUNCT_4:26;
then A3: stop I c= s2 +* (Initialized (stop I)) by A2, XBOOLE_1:1;
Initialized (stop I) c= s1 +* (Initialized (stop I)) by FUNCT_4:26;
then A4: stop I c= s1 +* (Initialized (stop I)) by A2, XBOOLE_1:1;
assume A5: DataPart s1 = DataPart s2 ; :: thesis: for k being Element of NAT holds
( Computation (s1 +* (Initialized (stop I))),k, Computation (s2 +* (Initialized (stop I))),k equal_outside NAT & CurInstr (Computation (s1 +* (Initialized (stop I))),k) = CurInstr (Computation (s2 +* (Initialized (stop I))),k) )

hereby :: thesis: verum

let k be Element of NAT ; :: thesis: ( Computation (s1 +* (Initialized (stop I))),k, Computation (s2 +* (Initialized (stop I))),k equal_outside NAT & CurInstr (Computation (s2 +* (Initialized (stop I))),k) = CurInstr (Computation (s1 +* (Initialized (stop I))),k) )
A6: IC (Computation (s1 +* (Initialized (stop I))),k) in dom (stop I) by A1, SCMPDS_6:def 2;
A7: I is_closed_on s2 by A1, A5, SCMPDS_6:36;
then A8: for m being Element of NAT st m < k holds
IC (Computation (s2 +* (Initialized (stop I))),m) in dom (stop I) by SCMPDS_6:def 2;
s1 +* (Initialized (stop I)),s2 +* (Initialized (stop I)) equal_outside NAT by A5, SCMPDS_6:12;
hence Computation (s1 +* (Initialized (stop I))),k, Computation (s2 +* (Initialized (stop I))),k equal_outside NAT by A4, A3, A8, SCMPDS_4:67; :: thesis: CurInstr (Computation (s2 +* (Initialized (stop I))),k) = CurInstr (Computation (s1 +* (Initialized (stop I))),k)
then A9: IC (Computation (s1 +* (Initialized (stop I))),k) = IC (Computation (s2 +* (Initialized (stop I))),k) by AMI_1:121;
A10: IC (Computation (s2 +* (Initialized (stop I))),k) in dom (stop I) by A7, SCMPDS_6:def 2;
thus CurInstr (Computation (s2 +* (Initialized (stop I))),k) = (s2 +* (Initialized (stop I))) . (IC (Computation (s2 +* (Initialized (stop I))),k)) by AMI_1:54
.= (stop I) . (IC (Computation (s2 +* (Initialized (stop I))),k)) by A3, A10, GRFUNC_1:8
.= (s1 +* (Initialized (stop I))) . (IC (Computation (s1 +* (Initialized (stop I))),k)) by A4, A9, A6, GRFUNC_1:8
.= CurInstr (Computation (s1 +* (Initialized (stop I))),k) by AMI_1:54 ; :: thesis: verum

end;