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

now

let x be set ; :: thesis: ( x in rng (aSeq (a,k)) implies b₁ in {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} )
assume A1: x in rng (aSeq (a,k)) ; :: thesis: b₁ in {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))}

per cases ( ( k > 0 & k = 0 + 1 ) or ( k > 0 & k <> 1 ) or not k > 0 ) ;

suppose A2: ( k > 0 & k = 0 + 1 ) ; :: thesis: b₁ in {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))}

then ex k1 being Element of NAT st
( k1 + 1 = k & aSeq (a,k) = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) by SCMFSA_7:def 2;
then aSeq (a,k) = <%(a := (intloc 0))%> ^ {} by A2
.= <%(a := (intloc 0))%> by AFINSQ_1:29 ;
then rng (aSeq (a,k)) = {(a := (intloc 0))} by AFINSQ_1:33;
then x = a := (intloc 0) by A1, TARSKI:def 1;
hence x in {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} by ENUMSET1:def 1; :: thesis: verum

end;

suppose A3: ( k > 0 & k <> 1 ) ; :: thesis: b₁ in {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))}

then consider k1 being Element of NAT such that
A4: k1 + 1 = k and
A5: aSeq (a,k) = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) by SCMFSA_7:def 2;
A6: k1 <> 0 by A3, A4;
rng (aSeq (a,k)) = (rng <%(a := (intloc 0))%>) \/ (rng (k1 --> (AddTo (a,(intloc 0))))) by A5, AFINSQ_1:26
.= {(a := (intloc 0))} \/ (rng (k1 --> (AddTo (a,(intloc 0))))) by AFINSQ_1:33
.= {(a := (intloc 0))} \/ {(AddTo (a,(intloc 0)))} by A6, FUNCOP_1:8 ;
then ( x in {(a := (intloc 0))} or x in {(AddTo (a,(intloc 0)))} ) by A1, XBOOLE_0:def 3;
then ( x = a := (intloc 0) or x = AddTo (a,(intloc 0)) ) by TARSKI:def 1;
hence x in {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} by ENUMSET1:def 1; :: thesis: verum

end;

suppose A7: not k > 0 ; :: thesis: b₁ in {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))}

then consider k1 being Element of NAT such that
A8: k1 + k = 1 and
A9: aSeq (a,k) = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) by SCMFSA_7:def 2;
A10: k1 <> 0 by A7, A8;
rng (aSeq (a,k)) = (rng <%(a := (intloc 0))%>) \/ (rng (k1 --> (SubFrom (a,(intloc 0))))) by A9, AFINSQ_1:26
.= {(a := (intloc 0))} \/ (rng (k1 --> (SubFrom (a,(intloc 0))))) by AFINSQ_1:33
.= {(a := (intloc 0))} \/ {(SubFrom (a,(intloc 0)))} by A10, FUNCOP_1:8 ;
then ( x in {(a := (intloc 0))} or x in {(SubFrom (a,(intloc 0)))} ) by A1, XBOOLE_0:def 3;
then ( x = a := (intloc 0) or x = SubFrom (a,(intloc 0)) ) by TARSKI:def 1;
hence x in {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} by ENUMSET1:def 1; :: thesis: verum

end;

end;

end;

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