Do we need Axiom of Choice to prove $|\prod_{i\in J}A_i| \le |\prod_{i\in I}A_i|$ for all $J \subseteq I$ where $I \setminus J$ is infinite? To prove the theorem, I try to define a injection $G:\prod\limits_{i\in J}A_i \to \prod\limits_{i\in I}A_i$. I'm able to define $G(\phi)$ for all $i \in J$ by $G(\phi)(i) = \phi(i)$. I feel that to define $G(\phi)$ for $i \in I \setminus J$ is impossible without AC in case $I \setminus J$ is infinite.

The Cartesian product of a family $(A_i\mid i\in I)$ is defined as $$\prod\limits_{i\in I}A_i=\{f:I\to\bigcup_{i \in I} A_i\mid f(i)\in A_i \text{ for all } i \in I\}$$

Theorem : Let $J \subseteq I$, then $|\prod\limits_{i\in J}A_i| \le |\prod\limits_{i\in I}A_i|$.


Consider
$$\begin
{array}{l|rcl}
G : & \prod\limits_{i\in J}A_i
 & \longrightarrow & \prod\limits_{i\in I}A_i \\
    & \phi & \longmapsto & G(\phi) \end{array}$$
where $\phi:J \to \bigcup_{i\in J}A_i$ such that $\phi(i) \in A_i$ for all $i \in J$.
$G(\phi)$ is defined by $G(\phi)(i) = \phi(i)$ for all $i \in J$.

Of course. It might just be that $\prod_{i\in I\setminus J} A_i$ is empty.
For example, take any $I'$ whose product is empty, and add $J$ as a family with a nonempty product, and $I=I'\cup J$.
If course, once you know that $\prod_{i\in I} A_i$ is nonempty, then the statement is true. Simply fix one choice function, and look at the modifications on $J$ given by the choice functions from $\prod_{i\in J} A_i$. 
