let R be good Ring; :: thesis: for s being State of (SCM R) holds Data-Locations SCM c= dom s
let s be State of (SCM R); :: thesis: Data-Locations SCM c= dom s
Data-Locations (SCM R) = Data-Locations SCM by SCMRING2:31;
hence Data-Locations SCM c= dom s by COMPOS_1:49; :: thesis: verum