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