let s be State of SCM+FSA; :: thesis: dom (s | Int-Locations) = Int-Locations
Int-Locations c= dom s by Th38;
hence dom (s | Int-Locations) = Int-Locations by RELAT_1:62; :: thesis: verum