let p be Function; :: thesis: for k being Element of NAT holds dom (Shift p,k) c= NAT
let k be Element of NAT ; :: thesis: dom (Shift p,k) c= NAT
A1: dom (Shift p,k) = { (m + k) where m is Element of NAT : m in dom p } by Def12;
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in dom (Shift p,k) or e in NAT )
assume e in dom (Shift p,k) ; :: thesis: e in NAT
then consider m being Element of NAT such that
A2: e = m + k and
m in dom p by A1;
thus e in NAT by A2; :: thesis: verum