theorem :: AMI_2:24

for k being Nat holds [1,k] in SCM-Data-Loc