:: deftheorem defines data-only MEMSTR_0:def 17 :
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for IT being PartFunc of (FinPartSt S),(FinPartSt S) holds
( IT is data-only iff for p being PartState of S st p in dom IT holds
( p is data-only & ( for q being PartState of S st q = IT . p holds
q is data-only ) ) );