let s be State of SCM; :: thesis: for d being Data-Location holds d in dom s
let d be Data-Location ; :: thesis: d in dom s
A: dom s = the carrier of SCM by PARTFUN1:def 2;
thus d in dom s by A; :: thesis: verum