deffunc H₁( Nat) -> set = p + k;
A1: dom p is finite ;
A2: { H₁(w) where w is Element of NAT : w in dom p } is finite from FRAENKEL:sch 21(A1);
dom (Shift (p,k)) c= { H₁(w) where w is Element of NAT : w in dom p }

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in dom (Shift (p,k)) or e in { H₁(w) where w is Element of NAT : w in dom p } )
assume e in dom (Shift (p,k)) ; :: thesis: e in { H₁(w) where w is Element of NAT : w in dom p }
then e in { H₁(i) where i is Nat : i in dom p } by Def12;
then consider i being Nat such that
A3: ( e = H₁(i) & i in dom p ) ;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
( e = H₁(i) & i in dom p ) by A3;
hence e in { H₁(w) where w is Element of NAT : w in dom p } ; :: thesis: verum

end;

hence Shift (p,k) is finite by A2, FINSET_1:10; :: thesis: verum