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