let p be non NAT -defined autonomic FinPartState of ; :: thesis: for s1, s2 being State of SCM+FSA 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 SCM+FSA ; :: 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 SCM+FSA ) = (Comput (ProgramPart s1),s1,i) . (IC SCM+FSA ) & ((Comput (ProgramPart s2),s2,i) | (dom p)) . (IC SCM+FSA ) = (Comput (ProgramPart s2),s2,i) . (IC SCM+FSA ) ) by Th15, FUNCT_1:72;
hence contradiction by A1, A2, A4, AMI_1:def 25; :: 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, Th17;
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, Th17;
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 AMI_1:150;
V: (ProgramPart (Comput (ProgramPart s1),s1,i)) /. (IC (Comput (ProgramPart s1),s1,i)) = (Comput (ProgramPart s1),s1,i) . (IC (Comput (ProgramPart s1),s1,i)) by AMI_1:150;
assume Z: 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, AMI_1:def 25;
hence contradiction by A3, A7, A6, Y, Z, V; :: thesis: verum

end;