:: deftheorem defines := SCMFSA_2:def 17 :
for c, i being Int-Location
for a being FinSeq-Location holds (a,i) := c = [10,{},<*c,a,i*>];