theorem Th5: :: SCMFSA_1:10

for b being Element of SCM+FSA-Data-Loc holds (SCM*-VAL * SCM+FSA-OK) . b = INT