let s be State of SCMPDS ; :: thesis: for l being Element of NAT holds l in dom s
let l be Element of NAT ; :: thesis: l in dom s
l in ({(IC SCMPDS )} \/ SCM-Data-Loc ) \/ NAT by XBOOLE_0:def 3;
hence l in dom s by PARTFUN1:def 4, SCMPDS_3:5; :: thesis: verum