A1: dom (Shift (p,k)) = { (m + k) where m is Nat : m in dom p } by Def12;
Shift (p,k) is NAT -defined
proof
let x be object ; :: according to TARSKI:def 3,RELAT_1:def 18 :: thesis: ( not x in dom (Shift (p,k)) or x in NAT )
assume x in dom (Shift (p,k)) ; :: thesis: x in NAT
then ex m being Nat st
( x = m + k & m in dom p ) by A1;
hence x in NAT by ORDINAL1:def 12; :: thesis: verum
end;
hence Shift (p,k) is NAT -defined ; :: thesis: verum