let N be non empty with_non-empty_elements set ; :: thesis: for k, m being natural number
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N
for I being Instruction of S holds IncAddr ((IncAddr (I,k)),m) = IncAddr (I,(k + m))
let k, m be natural number ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-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 homogeneous regular J/A-independent COM-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 Def38
.= InsCode I by Def38
.= InsCode (IncAddr (I,(k + m))) by Def38 ;
XX: AddressPart (IncAddr ((IncAddr (I,k)),m)) = AddressPart (IncAddr (I,k)) by Def38
.= AddressPart I by Def38
.= AddressPart (IncAddr (I,(k + m))) by Def38 ;
Y3: JumpPart (IncAddr ((IncAddr (I,k)),m)) = m + (JumpPart (IncAddr (I,k))) by Def38;
Y2: JumpPart (IncAddr (I,k)) = k + (JumpPart I) by Def38;
Y1: JumpPart (IncAddr (I,(k + m))) = (k + m) + (JumpPart I) by Def38;
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, Th7; :: thesis: verum