:: deftheorem defines :=len SCMFSA_2:def 18 :
for i being Int-Location
for a being FinSeq-Location holds i :=len a = [11,{},<*i,a*>];