let s be State of SCM+FSA ; :: thesis: Int-Locations c= dom s
dom s = the carrier of SCM+FSA by AMI_1:79;
hence Int-Locations c= dom s ; :: thesis: verum