let k be Element of NAT ; :: thesis: for p being FinPartState of SCM holds dom (ProgramPart (Relocated p,k)) = { (j + k) where j is Element of NAT : j in dom (ProgramPart p) }
let p be FinPartState of SCM ; :: thesis: dom (ProgramPart (Relocated p,k)) = { (j + k) where j is Element of NAT : j in dom (ProgramPart p) }
thus dom (ProgramPart (Relocated p,k)) = dom (IncAddr (Shift (ProgramPart p),k),k) by Th22
.= dom [(Shift (ProgramPart p),k)] by Def5
.= { (j + k) where j is Element of NAT : j in dom (ProgramPart p) } by VALUED_1:def 12 ; :: thesis: verum