Algebraic dual of a direct sum (source code)

= Algebraic dual of a direct sum
{title2=$(\bigoplus_iV_i)^*\cong\prod_iV_i^*$}

Restricting a <linear functional> to each summand gives a family of functionals, with no finite-support restriction. Conversely an arbitrary such family acts on a vector by the finite sum of its nonzero coordinates. These constructions are inverse and prove the displayed algebraic <dual space> identity. A group action on the summands induces the product action by their algebraic contragredients.