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