let S be non empty standard-ins homogeneous J/A-independent set ; for I being Element of S holds IncAddr (I,0) = I
let I be Element of S; IncAddr (I,0) = I
A1:
InsCode (IncAddr (I,0)) = InsCode I
by Def8;
A2:
AddressPart (IncAddr (I,0)) = AddressPart I
by Def8;
A3:
JumpPart (IncAddr (I,0)) = 0 + (JumpPart I)
by Def8;
then A4:
dom (JumpPart I) = dom (JumpPart (IncAddr (I,0)))
by VALUED_1:def 2;
for k being Nat st k in dom (JumpPart I) holds
(JumpPart (IncAddr (I,0))) . k = (JumpPart I) . k
then
JumpPart (IncAddr (I,0)) = JumpPart I
by A4;
hence
IncAddr (I,0) = I
by A1, A2, Th1; verum