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