theorem :: SCMFSA_2:26

for fa being FinSeq-Location
for a, c being Int-Location holds InsCode (c := (fa,a)) = 9 ;