let R be non trivial good Ring; :: thesis: for a being Data-Location of R
for p being PartState of (SCM R) st a in dom p holds
a in dom (NPP p)
let a be Data-Location of R; :: thesis: for p being PartState of (SCM R) st a in dom p holds
a in dom (NPP p)
let p be PartState of (SCM R); :: thesis: ( a in dom p implies a in dom (NPP p) )
Data-Locations (SCM R) = Data-Locations SCM by SCMRING2:31;
then A1: a in Data-Locations (SCM R) by SCMRING2:1;
assume a in dom p ; :: thesis: a in dom (NPP p)
then A2: a in dom (DataPart p) by A1, RELAT_1:86;
DataPart p c= NPP p by COMPOS_1:169;
then dom (DataPart p) c= dom (NPP p) by RELAT_1:25;
hence a in dom (NPP p) by A2; :: thesis: verum