for I being NAT -defined finite initial Function
for J being Function holds dom I misses dom (Shift (J,(card I)))