let a be Int-Location; :: thesis: for k being Integer holds a := k = (aSeq (a,k)) ^ (Stop SCM+FSA)
let k be Integer; :: thesis: a := k = (aSeq (a,k)) ^ (Stop SCM+FSA)

per cases ( k > 0 or k <= 0 ) ;

suppose k > 0 ; :: thesis: a := k = (aSeq (a,k)) ^ (Stop SCM+FSA)

then ex k1 being Nat st
( k1 + 1 = k & a := k = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) ) by Def1;
hence a := k = (aSeq (a,k)) ^ (Stop SCM+FSA) by Def2; :: thesis: verum

end;

suppose A1: k <= 0 ; :: thesis: a := k = (aSeq (a,k)) ^ (Stop SCM+FSA)

then ex k1 being Nat st
( k1 + k = 1 & a := k = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA) ) by Def1;
hence a := k = (aSeq (a,k)) ^ (Stop SCM+FSA) by A1, Def2; :: thesis: verum

end;

end;