theorem :: AMI_2:8

for a being Element of SCM-Data-Loc holds (SCM-VAL * SCM-OK) . a = INT by Th2;