let k, m be natural number ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for I being Instruction of S holds IncAddr (IncAddr I,k),m = IncAddr I,(k + m)
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,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 regular AMI-Struct of NAT ,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 ;
A2: dom (AddressPart (IncAddr I,(k + m))) = dom (AddressPart I) by Def14
.= dom (AddressPart (IncAddr I,k)) by Def14
.= dom (AddressPart (IncAddr (IncAddr I,k),m)) by Def14 ;
for n being set st n in dom (AddressPart (IncAddr (IncAddr I,k),m)) holds
(AddressPart (IncAddr (IncAddr I,k),m)) . n = (AddressPart (IncAddr I,(k + m))) . n

proof

let n be set ; :: thesis: ( n in dom (AddressPart (IncAddr (IncAddr I,k),m)) implies (AddressPart (IncAddr (IncAddr I,k),m)) . n = (AddressPart (IncAddr I,(k + m))) . n )
assume A3: n in dom (AddressPart (IncAddr (IncAddr I,k),m)) ; :: thesis: (AddressPart (IncAddr (IncAddr I,k),m)) . n = (AddressPart (IncAddr I,(k + m))) . n
A4: n in dom (AddressPart (IncAddr I,k)) by A3, Def14;
then A5: n in dom (AddressPart I) by Def14;

per cases ( (product" (AddressParts (InsCode I))) . n = NAT or (product" (AddressParts (InsCode I))) . n <> NAT ) ;

suppose A6: (product" (AddressParts (InsCode I))) . n = NAT ; :: thesis: (AddressPart (IncAddr (IncAddr I,k),m)) . n = (AddressPart (IncAddr I,(k + m))) . n

then consider f being Instruction-Location of S such that
A7: f = (AddressPart I) . n and
A8: (AddressPart (IncAddr I,k)) . n = il. S,(k + (locnum f)) by A5, Def14;
(product" (AddressParts (InsCode (IncAddr I,k)))) . n = NAT by A6, Th31;
then consider g being Instruction-Location of S such that
A9: g = (AddressPart (IncAddr I,k)) . n and
A10: (AddressPart (IncAddr (IncAddr I,k),m)) . n = il. S,(m + (locnum g)) by A4, Def14;
consider h being Instruction-Location of S such that
A11: h = (AddressPart I) . n and
A12: (AddressPart (IncAddr I,(k + m))) . n = il. S,((k + m) + (locnum h)) by A5, A6, Def14;
locnum g = k + (locnum f) by A8, A9, AMISTD_1:def 13;
hence (AddressPart (IncAddr (IncAddr I,k),m)) . n = (AddressPart (IncAddr I,(k + m))) . n by A7, A10, A11, A12; :: thesis: verum

end;

suppose A13: (product" (AddressParts (InsCode I))) . n <> NAT ; :: thesis: (AddressPart (IncAddr (IncAddr I,k),m)) . n = (AddressPart (IncAddr I,(k + m))) . n

then (product" (AddressParts (InsCode (IncAddr I,k)))) . n <> NAT by Def14;
hence (AddressPart (IncAddr (IncAddr I,k),m)) . n = (AddressPart (IncAddr I,k)) . n by A4, Def14
.= (AddressPart I) . n by A5, A13, Def14
.= (AddressPart (IncAddr I,(k + m))) . n by A5, A13, Def14 ;
:: thesis: verum

end;

end;

end;

hence IncAddr (IncAddr I,k),m = IncAddr I,(k + m) by A1, Th16, A2, FUNCT_1:9; :: thesis: verum