let k, m be Nat; :: thesis: for S being COM-Struct
for F being preProgram of S holds IncAddr ((IncAddr (F,k)),m) = IncAddr (F,(k + m))
let S be COM-Struct ; :: thesis: for F being preProgram of S holds IncAddr ((IncAddr (F,k)),m) = IncAddr (F,(k + m))
let F be preProgram of S; :: thesis: IncAddr ((IncAddr (F,k)),m) = IncAddr (F,(k + m))
A1: dom (IncAddr ((IncAddr (F,k)),m)) = dom (IncAddr (F,k)) by Def9
.= dom F by Def9 ;
A2: dom (IncAddr (F,(k + m))) = dom F by Def9;
for x being object st x in dom F holds
(IncAddr ((IncAddr (F,k)),m)) . x = (IncAddr (F,(k + m))) . x
proof
let x be object ; :: 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, Def9;
A5: IncAddr ((F /. x),k) = (IncAddr (F,k)) . x by A3, Def9
.= (IncAddr (F,k)) /. x by A4, PARTFUN1:def 6 ;
(IncAddr ((IncAddr (F,k)),m)) . x = IncAddr (((IncAddr (F,k)) /. x),m) by A4, Def9
.= IncAddr ((F /. x),(k + m)) by A5, COMPOS_0:7
.= (IncAddr (F,(k + m))) . x by A3, Def9 ;
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