for G being non empty 1-sorted
for a being Element of SCM-Data-Loc holds pi ((product ((SCM-VAL G) * SCM-OK)),a) = the carrier of G