Understanding a Result About Cosets 
I am trying to understand the above proof, particularly the line "For then by corollary 4.3. we must have $[G : K] = |I \times J|$, whence..." How do we know that the the number of all cosets of $K$ in $G$ is $|I \times J|$; how do we know that every coset arises as $Kb_j a_i$, where $\{a_i\}$ and $\{b_i\}$ are, I believe, minimal set of right coset representatives? 
Here is an attachment containing corollary 4.3: 

EDIT: 
Claim: Let $G$ be some group, $H$ some subgroup, and $M$ a nonempty subset of $G$. If $G = \sqcup_{g \in M} Hg$, then $M$ is a minimal set of right coset representatives (MSRCR).
Proof: Suppose the contrary, that $S \subseteq M$ is a MSRCR. Then there exists a $g' \in M \setminus S$. However, it is clearly the case that $G \setminus \sqcup_{g \in S} Hg = Hg'$, since all of the elements in $Hg'$ are not contained in any of the $Hg$ where $g \in S$. Hence, $M$ is the MSRCR. A corollary of this is that $|M| = [G : H]$.
Does this seem right; is this the idea needed to make the final conclusion? 
 A: "How do we know that every coset arises as $Kb_ja_i$ [...] ?"
This follows from the equality 
$$G = \bigcup_{(i,j)\in I\times J} Kb_ja_i$$
shown before. Thus every element from $G$ is in some coset $Kb_ja_i$, and so every coset of $K$ has the form $Kb_ja_i$.
(I think of the disjointness as follows: The disjoint decomposition $H=\bigcup_j Kb_j$ is mapped onto a disjoint decomposition $ Ha_i = \bigcup_j Kb_ja_i$ by multiplying everything with $a_i$ from the right. The disjointness is preserved because multiplying with a group element is an injective (in fact, bijective) map.)  
Edit (addressing comments and edit of OP):  Let $H$ be an arbitrary subgroup of $G$. By the corollary, two right cosets of $H$ are either equal, or they have no element in common. Thus the cosets partition $G$. By the definition that I know, a Minimal Set of Right Coset Representatives $M$ is defined by picking exactly one element from each coset. In other words, $M$ is a "MSRCR" if and only if $M$ contains exactly one element from each coset: $|M\cap Hg| = 1 $ for all $g\in G$. So I would say that $|M|= |G:H|$ by definition. And I would also say that this definition tells us that $M$ is a "MSRCR" if and only if $G =\bigsqcup_{m\in M} Hm$.
In your edit, you can only conclude that $Hg' \subseteq G\setminus \bigsqcup_{g\in S}Hg$, but otherwise the argument is correct. (I only think it is somewhat more complicated than needed.)
