theorem :: SCMFSA_2:28

for fa being FinSeq-Location
for a being Int-Location holds InsCode (a :=len fa) = 11 ;