let S be non empty standard-ins homogeneous J/A-independent set ; :: thesis: for I, J being Element of S st ex k being Nat st IncAddr (I,k) = IncAddr (J,k) holds
I = J

let I, J be Element of S; :: thesis: ( ex k being Nat st IncAddr (I,k) = IncAddr (J,k) implies I = J )
given k being Nat such that A1: IncAddr (I,k) = IncAddr (J,k) ; :: thesis: I = J
A2: InsCode I = InsCode (IncAddr (I,k)) by Def8
.= InsCode J by ;
.= AddressPart J by ;
A4: JumpPart (IncAddr (I,k)) = k + () by Def8;
then A5: dom () = dom (JumpPart (IncAddr (I,k))) by VALUED_1:def 2;
A6: JumpPart (IncAddr (J,k)) = k + () by Def8;
then A7: dom () = dom (JumpPart (IncAddr (J,k))) by VALUED_1:def 2;
A8: dom () = dom () by ;
for x being object st x in dom () holds
() . x = () . x
proof
let x be object ; :: thesis: ( x in dom () implies () . x = () . x )
assume A9: x in dom () ; :: thesis: () . x = () . x
A10: (JumpPart (IncAddr (I,k))) . x = k + (() . x) by ;
A11: (JumpPart (IncAddr (J,k))) . x = k + (() . x) by ;
thus (JumpPart I) . x = () . x by A1, A10, A11; :: thesis: verum
end;
then JumpPart I = JumpPart J by A8;
hence I = J by A2, A3, Th1; :: thesis: verum