theorem Th6: :: SCMFSA_1:11

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