let N be non empty with_non-empty_elements set ; :: thesis: for x being set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N st x in Data-Locations S holds
for p being PartState of S holds p . x = (NPP p) . x
let x be set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N st x in Data-Locations S holds
for p being PartState of S holds p . x = (NPP p) . x
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: ( x in Data-Locations S implies for p being PartState of S holds p . x = (NPP p) . x )
assume Z: x in Data-Locations S ; :: thesis: for p being PartState of S holds p . x = (NPP p) . x
let p be PartState of S; :: thesis: p . x = (NPP p) . x
DataPart p c= NPP p by Lm169;
then B: dom (DataPart p) c= dom (NPP p) by RELAT_1:25;
(Data-Locations S) /\ (dom p) = dom (DataPart p) by RELAT_1:90;
then (Data-Locations S) /\ (dom p) c= dom (NPP p) by B;
hence p . x = (NPP p) . x by Z, GRFUNC_1:97; :: thesis: verum