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 F being NAT -defined lower FinPartState of 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 regular AMI-Struct of N
for F being NAT -defined lower FinPartState of holds IncAddr (IncAddr F,k),m = IncAddr F,(k + m)
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of N; :: thesis: for F being NAT -defined lower FinPartState of holds IncAddr (IncAddr F,k),m = IncAddr F,(k + m)
let F be NAT -defined lower FinPartState of ; :: 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
dom F c= NAT by RELAT_1:def 18;
then reconsider x = x as Element of NAT by A3;
A4: x = il. S,(locnum x,S) by AMISTD_1:def 13;
then A5: il. S,(locnum x,S) in dom (IncAddr F,k) by A3, Def15;
A6: IncAddr (pi F,(il. S,(locnum x,S))),k = (IncAddr F,k) . (il. S,(locnum x,S)) by A3, A4, Def15
.= pi (IncAddr F,k),(il. S,(locnum x,S)) by A5, AMI_1:def 47 ;
(IncAddr (IncAddr F,k),m) . (il. S,(locnum x,S)) = IncAddr (pi (IncAddr F,k),(il. S,(locnum x,S))),m by A5, Def15
.= IncAddr (pi F,(il. S,(locnum x,S))),(k + m) by A6, Th37
.= (IncAddr F,(k + m)) . (il. S,(locnum x,S)) by A3, A4, Def15 ;
hence (IncAddr (IncAddr F,k),m) . x = (IncAddr F,(k + m)) . x by A4; :: thesis: verum

end;

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