let R be good Ring; :: thesis: Data-Locations (SCM R) = Data-Locations SCM
Data-Locations SCM misses {NAT} by AMI_2:27, AMI_3:72, ZFMISC_1:56;
then A1: Data-Locations SCM misses {NAT} \/ NAT by AMI_2:29, AMI_3:72, XBOOLE_1:70;
thus Data-Locations (SCM R) = SCM-Memory \ ({(IC (SCM R))} \/ NAT) by Def1
.= SCM-Memory \ ({NAT} \/ NAT) by Def1
.= ((Data-Locations SCM) \/ ({NAT} \/ NAT)) \ ({NAT} \/ NAT) by AMI_3:72, XBOOLE_1:4
.= (Data-Locations SCM) \ ({NAT} \/ NAT) by XBOOLE_1:40
.= Data-Locations SCM by A1, XBOOLE_1:83 ; :: thesis: verum