theorem :: MEMSTR_0:61

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for k being Nat
for p being PartState of S
for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds
p c= s1 +* (DataPart s2)