theorem Th5: :: AMI_2:10

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