let k, m be natural number ; :: thesis: for S being standard-ins homogeneous regular J/A-independent COM-Struct
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 standard-ins homogeneous regular J/A-independent COM-Struct ; :: 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 Def40
.= dom F by Def40 ;
A2: dom (IncAddr (F,(k + m))) = dom F by Def40;
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 12;
A4: x in dom (IncAddr (F,k)) by A3, Def40;
A5: IncAddr ((F /. x),k) = (IncAddr (F,k)) . x by A3, Def40
.= (IncAddr (F,k)) /. x by A4, PARTFUN1:def 6 ;
(IncAddr ((IncAddr (F,k)),m)) . x = IncAddr (((IncAddr (F,k)) /. x),m) by A4, Def40
.= IncAddr ((F /. x),(k + m)) by A5, Th97
.= (IncAddr (F,(k + m))) . x by A3, Def40 ;
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:2; :: thesis: verum