theorem :: SCMFSA_7:3

for a being Int-Location holds a := 0 = (<%(a := (intloc 0))%> ^ <%(SubFrom (a,(intloc 0)))%>) ^ (Stop SCM+FSA)