let k be Element of NAT ; :: thesis: for p being NAT -defined the Instructions of SCM -valued finite Function holds dom (Reloc p,k) = { (j + k) where j is Element of NAT : j in dom p }
let p be NAT -defined the Instructions of SCM -valued finite Function; :: thesis: dom (Reloc p,k) = { (j + k) where j is Element of NAT : j in dom p }
thus dom (Reloc p,k) = dom (Shift p,k) by Def5
.= { (j + k) where j is Element of NAT : j in dom p } by VALUED_1:def 12 ; :: thesis: verum