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