theorem :: SCMFSA_7:1

for a being Int-Location
for k being Integer holds a := k = (aSeq (a,k)) ^ (Stop SCM+FSA)