theorem :: VALUED_1:27

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