:: deftheorem defines intloc SCMFSA_2:def 6 :
for k being Nat holds intloc k = dl. k;