:: deftheorem defines :=<0,...,0> SCMFSA_2:def 19 :
for i being Int-Location
for a being FinSeq-Location holds a :=<0,...,0> i = [12,{},<*i,a*>];