dl. k in SCM+FSA-Data-Loc by AMI_3:def 2;
hence dl. k is Int-Location by Def4; :: thesis: verum