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 F being NAT -defined the Instructions of b₂ -valued finite Function holds IncAddr (IncAddr F,k),m = IncAddr F,(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 F being NAT -defined the Instructions of b₁ -valued finite Function holds IncAddr (IncAddr F,k),m = IncAddr F,(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 F being NAT -defined the Instructions of S -valued finite Function holds IncAddr (IncAddr F,k),m = IncAddr F,(k + m)
let F be NAT -defined the Instructions of S -valued finite Function; :: thesis: IncAddr (IncAddr F,k),m = IncAddr F,(k + m)
A1: dom (IncAddr (IncAddr F,k),m) = dom (IncAddr F,k) by Def15
.= dom F by Def15 ;
A2: dom (IncAddr F,(k + m)) = dom F by Def15;
for x being set st x in dom F holds
(IncAddr (IncAddr F,k),m) . x = (IncAddr F,(k + m)) . x

proof

let x be set ; :: thesis: ( x in dom F implies (IncAddr (IncAddr F,k),m) . x = (IncAddr F,(k + m)) . x )
assume A3: x in dom F ; :: thesis: (IncAddr (IncAddr F,k),m) . x = (IncAddr F,(k + m)) . x
reconsider x = x as Element of NAT by A3, ORDINAL1:def 13;
A5: x in dom (IncAddr F,k) by A3, Def15;
A6: IncAddr (F /. x),k = (IncAddr F,k) . x by A3, Def15
.= (IncAddr F,k) /. x by A5, PARTFUN1:def 8 ;
(IncAddr (IncAddr F,k),m) . x = IncAddr ((IncAddr F,k) /. x),m by A5, Def15
.= IncAddr (F /. x),(k + m) by A6, Th37
.= (IncAddr F,(k + m)) . x by A3, Def15 ;
hence (IncAddr (IncAddr F,k),m) . x = (IncAddr F,(k + m)) . x ; :: thesis: verum

end;

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