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
d in Data-Locations SCM by AMI_3:72, AMI_3:def 2;
then d in {(IC SCM)} \/ (Data-Locations SCM) by XBOOLE_0:def 3;
then d in ({(IC SCM)} \/ (Data-Locations SCM)) \/ NAT by XBOOLE_0:def 3;
hence d in dom s by AMI_3:4, AMI_3:72, PARTFUN1:def 4; :: thesis: verum