for t being FinSequence of INT
for f being FinSeq-Location holds dom (Initialize ((intloc 0) .--> 1)) misses dom (f .--> t)