let p be Function; :: thesis: for k, il being Element of NAT st il in dom p holds
il + k in dom (Shift (p,k))
let k be Element of NAT ; :: thesis: for il being Element of NAT st il in dom p holds
il + k in dom (Shift (p,k))
dom (Shift (p,k)) = { (loc + k) where loc is Element of NAT : loc in dom p } by Def12;
hence for il being Element of NAT st il in dom p holds
il + k in dom (Shift (p,k)) ; :: thesis: verum