for N being with_zero set
for S being Mem-Struct over N
for p being data-only PartState of S holds DataPart p = p