let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N
for I, J being Instruction of S st ex k being natural number st IncAddr I,k = IncAddr J,k holds
I = J
let S be non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N; :: thesis: for I, J being Instruction of S st ex k being natural number st IncAddr I,k = IncAddr J,k holds
I = J
let I, J be Instruction of S; :: thesis: ( ex k being natural number st IncAddr I,k = IncAddr J,k implies I = J )
given k being natural number such that A1: IncAddr I,k = IncAddr J,k ; :: thesis: I = J
A2: InsCode I = InsCode (IncAddr I,k) by Def14
.= InsCode J by A1, Def14 ;
XX: AddressPart I = AddressPart (IncAddr I,k) by Def14
.= AddressPart J by A1, Def14 ;
X1: JumpPart (IncAddr I,k) = k + (JumpPart I) by Def14;
then Y1: dom (JumpPart I) = dom (JumpPart (IncAddr I,k)) by VALUED_1:def 2;
X2: JumpPart (IncAddr J,k) = k + (JumpPart J) by Def14;
then Y2: dom (JumpPart J) = dom (JumpPart (IncAddr J,k)) by VALUED_1:def 2;
A3: dom (JumpPart I) = dom (JumpPart J) by A2, Def4;
for x being set st x in dom (JumpPart I) holds
(JumpPart I) . x = (JumpPart J) . x

proof

let x be set ; :: thesis: ( x in dom (JumpPart I) implies (JumpPart I) . x = (JumpPart J) . x )
assume A4: x in dom (JumpPart I) ; :: thesis: (JumpPart I) . x = (JumpPart J) . x
A7: (JumpPart (IncAddr I,k)) . x = k + ((JumpPart I) . x) by X1, Y1, A4, VALUED_1:def 2;
A9: (JumpPart (IncAddr J,k)) . x = k + ((JumpPart J) . x) by X2, A3, A4, Y2, VALUED_1:def 2;
thus (JumpPart I) . x = (JumpPart J) . x by A1, A7, A9; :: thesis: verum

end;

then JumpPart I = JumpPart J by A3, FUNCT_1:9;
hence I = J by A2, XX, COMPOS_1:7; :: thesis: verum