theorem Th76: :: AFINSQ_1:79

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