:: deftheorem defines on_data_only MEMSTR_0:def 18 :
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for f being Function of (product (the_Values_of S)),NAT holds
( f is on_data_only iff for s1, s2 being State of S st DataPart s1 = DataPart s2 holds
f . s1 = f . s2 );