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

proof

assume A5: IC (Computation s1,i) <> IC (Computation s2,i) ; :: thesis: contradiction
( ((Computation s1,i) | (dom p)) . (IC SCM ) = (Computation s1,i) . (IC SCM ) & ((Computation s2,i) | (dom p)) . (IC SCM ) = (Computation s2,i) . (IC SCM ) ) by Th84, FUNCT_1:72;
hence contradiction by A1, A2, A5, AMI_1:def 25; :: thesis: verum

end;

thus I = CurInstr (Computation s2,i) :: thesis: verum

proof

ProgramPart p c= p by RELAT_1:88;
then A6: dom (ProgramPart p) c= dom p by GRFUNC_1:8;
IC (Computation s2,i) in dom (ProgramPart p) by A2, Th86;
then A7: ((Computation s2,i) | (dom p)) . (IC (Computation s2,i)) = (Computation s2,i) . (IC (Computation s2,i)) by A6, FUNCT_1:72;
IC (Computation s1,i) in dom (ProgramPart p) by A1, Th86;
then A8: ((Computation s1,i) | (dom p)) . (IC (Computation s1,i)) = (Computation s1,i) . (IC (Computation s1,i)) by A6, FUNCT_1:72;
assume I <> CurInstr (Computation s2,i) ; :: thesis: contradiction
hence contradiction by A1, A2, A3, A4, A8, A7, AMI_1:def 25; :: thesis: verum

end;