Deriving recursive definition from function specification
Your notation and understanding are pretty good. 

It is easier to consider (xs:x) as the inductive case instead of (x:xs)

\begin{align}
\sum_{i:\ 0 \leq i &lt; \#(xs:x)} &amp;(xs:x).i * (i + 1)\\
&amp;=\sum _{i:\ 0 \leq i &lt; \#xs+1} (x:xs).i * (i + 1) \\
&amp;=\sum_{i:\ 0 \leq i &lt; \#xs} (xs:x).i * (i + 1)+\sum_{i:\ i=\#xs}(xs:x).i * (i + 1)\\
&amp;=\sum_{i:\ 0 \leq i &lt; \#xs} xs.i * (i + 1)+x*(\#xs+1),\\
\end{align}
where we assume that list index starts with 0.

If we denote the function by $f$, the above equality becomes 
$$ f(xs:x) = f(xs) + x*(\#xs+1), $$
which is the recursive step of a recursive definition.

The base case, as you have indicated, is 
$$ f([]) =  \sum_{ i:\ 0 \leq i &lt; 0} [].i * (i + 1)  =  \sum_{i: \text{ empty set}}[].i * (i + 1) =0.$$



Exercise. Derive the following recursive formula of the same function $f$.
$$ f(x:xs) = f(xs) + t(xs)+ x, $$
where $$t(xs)=\sum_{i:\ 0 \leq i &lt; \#(xs)} xs.i,$$
the sum of items in $xs$.