A1: Int-Locations = SCM+FSA-Data-Loc ;
dl. k in SCM-Data-Loc by AMI_2:def 16;
hence dl. k is Int-Location by A1; :: thesis: verum