let l be Nat; :: thesis: UsedILoc (Goto l) = {}
Goto l = Load (goto l) by SCMFSA8A:def 1;
hence UsedILoc (Goto l) = UsedIntLoc (goto l) by Th1
.= {} by SF_MASTR:15 ;
:: thesis: verum