for a being Element of SCM-Data-Loc holds pi ((product (SCM-VAL * SCM-OK)),a) = INT