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)))}
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (aSeq (a,k)) or x in {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} )
assume A1: x in rng (aSeq (a,k)) ; :: thesis: x 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: x in {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))}

then ex k1 being 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))%> ;
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: x in {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))}

then consider k1 being 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: x in {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))}

then consider k1 being 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;