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