let p be preProgram of SCM+FSA ; :: 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 ;
A2: l = insloc m ;
thus (IncAddr p,k) . l = IncAddr (pi p,l),k by A1, A2, Def6; :: thesis: verum