for d1 being Element of SCM-Data-Loc
for G being non empty 1-sorted holds ((SCM-VAL G) * SCM-OK) . d1 = the carrier of G by Th2;