theorem :: SCMFSA_M:29

for x being set
for i, m, n being Nat holds
( not x in dom (((intloc i) .--> m) +* (Start-At (n,SCM+FSA))) or x = intloc i or x = IC )