reconsider k = k as Element of NAT by ORDINAL1:def 12;
1 in {1} by TARSKI:def 1;
then [1,k] in SCM-Data-Loc by ZFMISC_1:87;
hence [1,k] is Data-Location by AMI_2:def 16; :: thesis: verum