A1: dom (Shift p,k) = { (m + k) where m is Element of NAT : m in dom p } by Def12;
Shift p,k is NAT -defined

proof

let x be set ; :: according to TARSKI:def 3,RELAT_1:def 18 :: thesis: ( not x in proj1 (Shift p,k) or x in NAT )
assume x in dom (Shift p,k) ; :: thesis: x in NAT
then ex m being Element of NAT st
( x = m + k & m in dom p ) by A1;
hence x in NAT ; :: thesis: verum

end;

hence Shift p,k is NAT -defined ; :: thesis: verum