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