for f being Element of SCM+FSA-Data*-Loc holds (SCM*-VAL * SCM+FSA-OK) . f = INT *