let R be good Ring; :: thesis: for p being FinPartState of (SCM R) holds dom (DataPart p) c= SCM-Data-Loc
let p be FinPartState of (SCM R); :: thesis: dom (DataPart p) c= SCM-Data-Loc
Data-Locations (SCM R) = SCM-Data-Loc by SCMRING2:31;
hence dom (DataPart p) c= SCM-Data-Loc by RELAT_1:87; :: thesis: verum