let k, m be natural number ; :: thesis: for N being non empty with_non-empty_elements set
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 being Instruction of S holds IncAddr (IncAddr I,k),m = IncAddr I,(k + m)
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 being Instruction of S holds IncAddr (IncAddr I,k),m = IncAddr I,(k + m)
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 being Instruction of S holds IncAddr (IncAddr I,k),m = IncAddr I,(k + m)
let I be Instruction of S; :: thesis: IncAddr (IncAddr I,k),m = IncAddr I,(k + m)
A1: InsCode (IncAddr (IncAddr I,k),m) = InsCode (IncAddr I,k) by Def14
.= InsCode I by Def14
.= InsCode (IncAddr I,(k + m)) by Def14 ;
XX: AddressPart (IncAddr (IncAddr I,k),m) = AddressPart (IncAddr I,k) by Def14
.= AddressPart I by Def14
.= AddressPart (IncAddr I,(k + m)) by Def14 ;
Y3: JumpPart (IncAddr (IncAddr I,k),m) = m + (JumpPart (IncAddr I,k)) by Def14;
Y2: JumpPart (IncAddr I,k) = k + (JumpPart I) by Def14;
Y1: JumpPart (IncAddr I,(k + m)) = (k + m) + (JumpPart I) by Def14;
then A2: dom (JumpPart (IncAddr I,(k + m))) = dom (JumpPart I) by VALUED_1:def 2
.= dom (JumpPart (IncAddr I,k)) by Y2, VALUED_1:def 2
.= dom (JumpPart (IncAddr (IncAddr I,k),m)) by Y3, VALUED_1:def 2 ;
for n being set st n in dom (JumpPart (IncAddr (IncAddr I,k),m)) holds
(JumpPart (IncAddr (IncAddr I,k),m)) . n = (JumpPart (IncAddr I,(k + m))) . n

proof

let n be set ; :: thesis: ( n in dom (JumpPart (IncAddr (IncAddr I,k),m)) implies (JumpPart (IncAddr (IncAddr I,k),m)) . n = (JumpPart (IncAddr I,(k + m))) . n )
assume Z: n in dom (JumpPart (IncAddr (IncAddr I,k),m)) ; :: thesis: (JumpPart (IncAddr (IncAddr I,k),m)) . n = (JumpPart (IncAddr I,(k + m))) . n
then A3: n in dom (JumpPart (IncAddr I,k)) by Y3, VALUED_1:def 2;
then A4: n in dom (JumpPart I) by Y2, VALUED_1:def 2;
A7: (JumpPart (IncAddr I,k)) . n = k + ((JumpPart I) . n) by Y2, A3, VALUED_1:def 2;
A9: (JumpPart (IncAddr (IncAddr I,k),m)) . n = m + ((JumpPart (IncAddr I,k)) . n) by Z, Y3, VALUED_1:def 2;
n in dom (JumpPart (IncAddr I,(k + m))) by Y1, A4, VALUED_1:def 2;
then (JumpPart (IncAddr I,(k + m))) . n = (k + m) + ((JumpPart I) . n) by Y1, VALUED_1:def 2;
hence (JumpPart (IncAddr (IncAddr I,k),m)) . n = (JumpPart (IncAddr I,(k + m))) . n by A9, A7; :: thesis: verum

end;

then JumpPart (IncAddr (IncAddr I,k),m) = JumpPart (IncAddr I,(k + m)) by A2, FUNCT_1:9;
hence IncAddr (IncAddr I,k),m = IncAddr I,(k + m) by A1, XX, COMPOS_1:7; :: thesis: verum