for N being with_zero set
for S being Mem-Struct over N
for p being PartState of S holds {(IC )} misses dom (DataPart p) by Th3, ZFMISC_1:50;