let S be COM-Struct ; :: thesis: for k being Nat
for p being NAT -defined the InstructionsF of S -valued finite Function holds dom (Reloc (p,k)) = { (j + k) where j is Nat : j in dom p }
let k be Nat; :: thesis: for p being NAT -defined the InstructionsF of S -valued finite Function holds dom (Reloc (p,k)) = { (j + k) where j is Nat : j in dom p }
let p be NAT -defined the InstructionsF of S -valued finite Function; :: thesis: dom (Reloc (p,k)) = { (j + k) where j is Nat : j in dom p }
thus dom (Reloc (p,k)) = dom (Shift (p,k)) by Th20
.= { (j + k) where j is Nat : j in dom p } by VALUED_1:def 12 ; :: thesis: verum