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 3;
then aSeq a,k = <*(a := (intloc 0 ))*> ^ {} by A2
.= <*(a := (intloc 0 ))*> by FINSEQ_1:47 ;
then rng (aSeq a,k) = {(a := (intloc 0 ))} by FINSEQ_1:55;
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 3;
A6: k1 <> 0 by A3, A4;
rng (aSeq a,k) = (rng <*(a := (intloc 0 ))*>) \/ (rng (k1 |-> (AddTo a,(intloc 0 )))) by A5, FINSEQ_1:44
.= {(a := (intloc 0 ))} \/ (rng ((Seg k1) --> (AddTo a,(intloc 0 )))) by FINSEQ_1:55
.= {(a := (intloc 0 ))} \/ {(AddTo a,(intloc 0 ))} by A6, FUNCOP_1:14 ;
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 3;
A10: k1 <> 0 by A7, A8;
rng (aSeq a,k) = (rng <*(a := (intloc 0 ))*>) \/ (rng (k1 |-> (SubFrom a,(intloc 0 )))) by A9, FINSEQ_1:44
.= {(a := (intloc 0 ))} \/ (rng ((Seg k1) --> (SubFrom a,(intloc 0 )))) by FINSEQ_1:55
.= {(a := (intloc 0 ))} \/ {(SubFrom a,(intloc 0 ))} by A10, FUNCOP_1:14 ;
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