let p be preProgram of ; :: thesis: for k, l being Element of NAT st l in dom p holds
(IncAddr p,k) . l = IncAddr (pi p,l),k
let k, l be Element of NAT ; :: thesis: ( l in dom p implies (IncAddr p,k) . l = IncAddr (pi p,l),k )
assume A1: l in dom p ; :: thesis: (IncAddr p,k) . l = IncAddr (pi p,l),k
reconsider m = l as Element of NAT ;
l = insloc m ;
hence (IncAddr p,k) . l = IncAddr (pi p,l),k by A1, Def6; :: thesis: verum