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)))}
let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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) ; :: 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