theorem :: FUNCT_7:133

for m being Nat
for I being NAT -defined Function holds card (Shift (I,m)) = card I