:: deftheorem defines UsedILoc SF_MASTR:def 3 :
for p being Function holds UsedILoc p = UsedILoc (rng p);