deffunc H₁( Element of NAT ) -> Element of NAT = p + k;
A1: dom p is finite ;
{ H₁(w) where w is Element of NAT : w in dom p } is finite from FRAENKEL:sch 21(A1);
then dom (Shift p,k) is finite by Def12;
hence Shift p,k is finite by FINSET_1:29; :: thesis: verum