let a be Int-Location ; :: thesis: 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; :: thesis: rng (a := k) c= {(halt SCM+FSA),(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))}

now

let x be set ; :: thesis: ( x in rng (a := k) implies 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 Th29;
A2: rng (a := k) = rng ((aSeq (a,k)) ^ <%(halt SCM+FSA)%>) by SCMFSA_7:1
.= (rng (aSeq (a,k))) \/ (rng <%(halt SCM+FSA)%>) by AFINSQ_1:26
.= (rng (aSeq (a,k))) \/ {(halt SCM+FSA)} by AFINSQ_1:33 ;
assume x in rng (a := k) ; :: thesis: 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; :: thesis: verum

end;

hence rng (a := k) c= {(halt SCM+FSA),(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} by TARSKI:def 3; :: thesis: verum