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