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