let l be Nat; :: thesis: UsedI*Loc (Goto l) = {}
Goto l = Load (goto l) by SCMFSA8A:def 1;
hence UsedI*Loc (Goto l) = UsedInt*Loc (goto l) by Th2
.= {} by SF_MASTR:32 ;
:: thesis: verum