let m, n be Element of NAT ; :: thesis: for I being preProgram of holds IncAddr (IncAddr I,m),n = IncAddr I,(m + n)
let I be preProgram of ; :: thesis: IncAddr (IncAddr I,m),n = IncAddr I,(m + n)
A1: dom (IncAddr I,m) = dom I by Def6;

A2: now

let l be Element of NAT ; :: thesis: ( insloc l in dom I implies (IncAddr (IncAddr I,m),n) . (insloc l) = IncAddr (pi I,l),(m + n) )
assume A3: insloc l in dom I ; :: thesis: (IncAddr (IncAddr I,m),n) . (insloc l) = IncAddr (pi I,l),(m + n)
then pi (IncAddr I,m),l = (IncAddr I,m) . (insloc l) by A1, AMI_1:def 47
.= IncAddr (pi I,l),m by A3, Th24 ;
hence (IncAddr (IncAddr I,m),n) . (insloc l) = IncAddr (IncAddr (pi I,l),m),n by A1, A3, Th24
.= IncAddr (pi I,l),(m + n) by Th23 ;
:: thesis: verum

end;

dom (IncAddr (IncAddr I,m),n) = dom (IncAddr I,m) by Def6;
hence IncAddr (IncAddr I,m),n = IncAddr I,(m + n) by A1, A2, Def6; :: thesis: verum