let a be Int-Location; for k being Integer holds rng (a := k) c= {(halt SCM+FSA),(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))}
let k be Integer; rng (a := k) c= {(halt SCM+FSA),(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))}
let x be object ; TARSKI:def 3 ( not x in rng (a := k) or x in {(halt SCM+FSA),(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} )
A1:
rng (aSeq (a,k)) c= {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))}
by Th21;
A2: rng (a := k) =
rng ((aSeq (a,k)) ^ (Stop SCM+FSA))
by SCMFSA_7:1
.=
(rng (aSeq (a,k))) \/ (rng (Stop SCM+FSA))
by AFINSQ_1:26
.=
(rng (aSeq (a,k))) \/ {(halt SCM+FSA)}
by AFINSQ_1:33
;
assume
x in rng (a := k)
; x in {(halt SCM+FSA),(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))}
then
( x in rng (aSeq (a,k)) or x in {(halt SCM+FSA)} )
by A2, XBOOLE_0:def 3;
then
( x = a := (intloc 0) or x = AddTo (a,(intloc 0)) or x = SubFrom (a,(intloc 0)) or x = halt SCM+FSA )
by A1, ENUMSET1:def 1, TARSKI:def 1;
hence
x in {(halt SCM+FSA),(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))}
by ENUMSET1:def 2; verum