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 ))} )
assume A1: x in rng (a := k) ; :: thesis: x in {(halt SCM+FSA ),(a := (intloc 0 )),(AddTo a,(intloc 0 )),(SubFrom a,(intloc 0 ))}
a := k = Load ((aSeq a,k) ^ <*(halt SCM+FSA )*>) by SCMFSA_7:33;
then rng (a := k) = rng ((aSeq a,k) ^ <*(halt SCM+FSA )*>) by Th2
.= (rng (aSeq a,k)) \/ (rng <*(halt SCM+FSA )*>) by FINSEQ_1:44
.= (rng (aSeq a,k)) \/ {(halt SCM+FSA )} by FINSEQ_1:55 ;
then A2: ( x in rng (aSeq a,k) or x in {(halt SCM+FSA )} ) by A1, XBOOLE_0:def 3;
rng (aSeq a,k) c= {(a := (intloc 0 )),(AddTo a,(intloc 0 )),(SubFrom a,(intloc 0 ))} by Th29;
then ( x = a := (intloc 0 ) or x = AddTo a,(intloc 0 ) or x = SubFrom a,(intloc 0 ) or x = halt SCM+FSA ) by A2, 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