theorem Th7: :: SCMFSA_2:12

for l being FinSeq-Location holds Values l = INT *