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
A1: dom s = the carrier of SCM by PARTFUN1:def 2;
thus d in dom s by A1; :: thesis: verum