let da be Int-Location ; :: thesis: for p being PartState of SCM+FSA st da in dom p holds
da in dom (NPP p)
let p be PartState of SCM+FSA; :: thesis: ( da in dom p implies da in dom (NPP p) )
da in Int-Locations by SCMFSA_2:9;
then A1: da in Data-Locations SCM+FSA by SCMFSA_2:127, XBOOLE_0:def 3;
assume da in dom p ; :: thesis: da in dom (NPP p)
then A2: da 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 da in dom (NPP p) by A2; :: thesis: verum