If $K,H,G$ are groups with $K\lt H \lt G$, then $[G:K]=[G:H][H:K]$. If any two of these indices are finite, then so is the third.
Proof: By Corollary 4.3 $G= \bigcup_{i\in I}Ha_i$ with $a_i \in G$, $|I|=[G:H]$ and the cosets $Ha_i$ mutually disjoint (that is, $Ha_i = Ha_j \Leftrightarrow i=j$). Similarly $H=\bigcup_{j\in J} Kb_j$ with $b_j\in H$, $|J|=[H: K]$ and the cosets $Kb_j$ are mutually disjoint. Therefore $G=\bigcup_{i\in I}Ha_i=\bigcup_{i\in J} (\bigcup_{j\in J}Kb_j)a_i=\bigcup_{(i,j)\in I\times J}Kb_ja_i$. It suffices to show that the cosets $Kb_ja_i$ are mutually disjoint. For then by Corollary 4.3. we must have $[G:K]=|I\times J|$, whence $[G:K]=|I\times J|=|I||J|=[G:H][H:K]$. If $Kb_ja_i=Kb_ra_t$, then $b_ja_i=kb_ra_t$ ($k\in K$). Since $b_j,b_r,k\in H$ we have $Ha_i = Hb_ja_i = Hkb_ra_t = Ha_t$; hence $i = t$ and $b_j=kb_r$. Thus $Kb_j=Kkb_r=Kb_r$ and $j = r$. Therefore, the cosets $Kb_ja_i$ are mutually disjoint. The last statement of the theorem is obvious.
Question: Let $P=\{Kb_ja_i\mid (i,j)\in I\times J\}$ and $Q=\{Kc\mid c\in G\}$. I think $G=\bigcup_{(i,j)\in I\times J}Kb_ja_i$ shows $P=Q$ and $P$ is pairwise disjoint shows $|P|=|I\times J|$.
We claim $P=Q$. Clearly $P\subseteq Q$. Conversely, let $Kd\in Q$ for some $d\in G$. Then $Kd\subseteq G=\bigcup_{(i,j)\in I\times J}Kb_ja_i$. So $d=ed\in Kb_qa_p$, for some $(p,q)\in I\times J$. Thus $Kd\cap Kb_qa_p\neq \emptyset$. Since two equivalence class are either disjoint or equal, we have $Kd= Kb_qa_p$. Hence $Kd\in P$ and $P\supseteq Q$. So $P=Q$. Is my proof correct? It is clear that $P$ is partition of $G$. Can we use partition argument to prove $[G:K]=|I\times J|$? I mean equivalence relation defined by partition $P$ is same as right congruence modulo $K$.
How to rigioursly prove $|I\times J|=|I||J|$? For $|I\times J|=|I||J|$ to make sense, we need to define “multiplication” in $\Bbb{N}\cup \{+\infty \}$.
Author also didn’t include details of $(\bigcup_{j\in J}Kb_j)a_i= \bigcup_{j\in J}Kb_ja_i$ and $\bigcup_{i\in J}\bigcup_{j\in J}Kb_ja_i=\bigcup_{(i,j)\in I\times J}Kb_ja_i$ and $Hb=H$, for all $b\in H$, though these are easy to verify.
Your proof is correct, yes, but I don't see why you need it. For your other questions:
$i):$ The fact that $[G:K]=|I\times J|$ follows directly from $G=\bigcup_{(i,j)\in I\times J}Kb_ja_i$ using Corollary $4.3$. You don't need a partition argument.
$ii):$ Multiplication in $\mathbb{N}\cup\lbrace\infty\rbrace$ is simple: when $a,b\in\mathbb{N}$, $a\cdot b$ is computed as usual, and if $a=\infty$ and/or $b=\infty$, then we define $a\cdot b=\infty$. This is consistent with $|I\times J|=|I|\cdot |J|$. If $I$ or $J$ is infinite, then so is $I\times J$. If they are both finite, given $i_0\in I$ define $J_{i_0}=\lbrace (i_0,j)\mid j\in J\rbrace\subset I\times J$. It is clear that $|J|=|J_{i_0}|$. then you have a disjoint finite union $I\times J = \bigcup_{i\in I}J_i$, and since it is disjoint, you get the cardinality formula $|I\times J| = \left|\bigcup_{i\in I}J_i\right| = \prod_{i\in I}|J_i|=|I|\cdot |J|$. This is basic set theory.