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 regular 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 regular 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 regular 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 ;
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 n in dom (AddressPart (IncAddr (IncAddr I,k),m)) ; :: thesis: (AddressPart (IncAddr (IncAddr I,k),m)) . n = (AddressPart (IncAddr I,(k + m))) . n
then A3: n in dom (AddressPart (IncAddr I,k)) by Def14;
then A4: n in dom (AddressPart I) by Def14;

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

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

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

end;

suppose A11: (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 A3, Def14
.= (AddressPart I) . n by A4, A11, Def14
.= (AddressPart (IncAddr I,(k + m))) . n by A4, A11, Def14 ;
:: thesis: verum

end;

end;

end;

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