let s be State of SCM+FSA; :: thesis: for d being Int-Location holds d in dom s
let d be Int-Location; :: thesis: d in dom s
dom s = the carrier of SCM+FSA by PARTFUN1:def 2;
hence d in dom s ; :: thesis: verum