let p be non NAT -defined autonomic FinPartState of ; :: thesis: for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 holds
for i being Element of NAT holds
( IC (Comput ((ProgramPart s1),s1,i)) = IC (Comput ((ProgramPart s2),s2,i)) & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) )
let s1, s2 be State of SCMPDS; :: thesis: ( p c= s1 & p c= s2 implies for i being Element of NAT holds
( IC (Comput ((ProgramPart s1),s1,i)) = IC (Comput ((ProgramPart s2),s2,i)) & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) ) )
assume that
A1: p c= s1 and
A2: p c= s2 ; :: thesis: for i being Element of NAT holds
( IC (Comput ((ProgramPart s1),s1,i)) = IC (Comput ((ProgramPart s2),s2,i)) & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) )
let i be Element of NAT ; :: thesis: ( IC (Comput ((ProgramPart s1),s1,i)) = IC (Comput ((ProgramPart s2),s2,i)) & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) )
set Cs1i = Comput ((ProgramPart s1),s1,i);
set Cs2i = Comput ((ProgramPart s2),s2,i);
thus A3: IC (Comput ((ProgramPart s1),s1,i)) = IC (Comput ((ProgramPart s2),s2,i)) :: thesis: CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i)))

proof

assume A4: IC (Comput ((ProgramPart s1),s1,i)) <> IC (Comput ((ProgramPart s2),s2,i)) ; :: thesis: contradiction
( ((Comput ((ProgramPart s1),s1,i)) | (dom p)) . (IC SCMPDS) = (Comput ((ProgramPart s1),s1,i)) . (IC SCMPDS) & ((Comput ((ProgramPart s2),s2,i)) | (dom p)) . (IC SCMPDS) = (Comput ((ProgramPart s2),s2,i)) . (IC SCMPDS) ) by Th17, FUNCT_1:72;
hence contradiction by A1, A2, A4, EXTPRO_1:def 9; :: thesis: verum

end;

set I = CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)));
thus CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) :: thesis: verum

proof

ProgramPart p c= p by RELAT_1:88;
then A5: dom (ProgramPart p) c= dom p by GRFUNC_1:8;
IC (Comput ((ProgramPart s2),s2,i)) in dom (ProgramPart p) by A2, Th22;
then A6: ((Comput ((ProgramPart s2),s2,i)) | (dom p)) . (IC (Comput ((ProgramPart s2),s2,i))) = (Comput ((ProgramPart s2),s2,i)) . (IC (Comput ((ProgramPart s2),s2,i))) by A5, FUNCT_1:72;
IC (Comput ((ProgramPart s1),s1,i)) in dom (ProgramPart p) by A1, Th22;
then A7: ((Comput ((ProgramPart s1),s1,i)) | (dom p)) . (IC (Comput ((ProgramPart s1),s1,i))) = (Comput ((ProgramPart s1),s1,i)) . (IC (Comput ((ProgramPart s1),s1,i))) by A5, FUNCT_1:72;
Y: (ProgramPart (Comput ((ProgramPart s2),s2,i))) /. (IC (Comput ((ProgramPart s2),s2,i))) = (Comput ((ProgramPart s2),s2,i)) . (IC (Comput ((ProgramPart s2),s2,i))) by COMPOS_1:38;
Z: (ProgramPart (Comput ((ProgramPart s1),s1,i))) /. (IC (Comput ((ProgramPart s1),s1,i))) = (Comput ((ProgramPart s1),s1,i)) . (IC (Comput ((ProgramPart s1),s1,i))) by COMPOS_1:38;
assume ZZ: CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) <> CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) ; :: thesis: contradiction
(Comput ((ProgramPart s1),s1,i)) | (dom p) = (Comput ((ProgramPart s2),s2,i)) | (dom p) by A1, A2, EXTPRO_1:def 9;
hence contradiction by A3, A7, A6, Y, ZZ, Z; :: thesis: verum

end;