theorem Th21: :: SCMFSA7B:22

for a being Int-Location
for k being Integer holds rng (aSeq (a,k)) c= {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))}