for k being Nat
for F being NAT -defined Function holds dom F, dom (Shift (F,k)) are_equipotent