theorem Th6: :: SCMFSA9A:6

for l being Nat holds UsedI*Loc (Goto l) = {}