for w being FinSequence of INT
for f being FinSeq-Location holds dom (Initialized (f .--> w)) = {(intloc 0),(IC ),f}