theorem :: SFMASTR3:36

for aa, bb being Int-Location
for f being FinSeq-Location holds UsedI*Loc (swap (f,aa,bb)) = {f}