Sirous agreed to do this in class. He put up a proof of the orbit stabilizer theorem that showed the map $\phi : G/G_s \rightarrow O_s$ defined by $\phi( g G_s ) = g s$ was well defined, 11 and onto. 
Farid agreed to do this in class. I didn't copy exactly what he wrote, but I will try
to recall the details that he added. He actually went further and proved: Machke's Theorem: If $G$ is a finite group and a $V$ is a $G$module over ${\mathbb C}$, then $$V = W_1 \oplus W_2 \oplus \cdots \oplus W_k$$ where each of the $W_i$ are irreducible $G$submodules. 
Lemma 1: Let $\{ v_1, v_2, \ldots, v_n \}$ be a basis for $V$, then set
$\left< v_i, v_j \right> = \begin{cases}
1&\hbox{ if }i=j\\
0&\hbox{ else }
\end{cases}.$ $\left< u,v \right>$ is a inner product.

(Proof of Lemma 1): We need to show that (a) $\left< u, v \right> = {\overline {\left< v, u \right>}}$, (b) $\left< a v + b w, u \right> = a \left< v, u \right> + b \left< w, u\right>$ and (c) $\left< v, v \right> > 0$ if $v \neq {\bf 0}$. We can ensure that that (a) and (b) hold by definition since we have defined this scalar product on a basis. (c) holds because if $v = \sum_{i=1}^n c_i v_i$, then $\left< v, v\right> = \sum_{i=1}^n c_i {\overline c_i}$ and this is a positive number as long as it is not the case that $v = {\bf 0}$. 
Lemma 2: Let $\left< u, v \right>$ be the inner product defined in Lemma 1, then
either this inner product is $G$ invariant or $\left< u, v \right>' =
\sum_{g \in G} \left< g u, g v \right>$ is a $G$ invariant inner product.

(Outline of proof of Lemma 2): Assume that $\left< u, v \right>$ as defined in
Lemma 1 is not $G$invariant, then
$$\left< hu, hv \right>'
= \sum_{g \in G} \left< gh u, gh v \right> = \sum_{k in G} \left< k u, k v \right>
= \left< u, v \right>'~.$$
Next show that $\left< u, v \right>'$ satisfies the conditions of a scalar product
(a), (b), (c) as in the proof of Lemma 1. The details are left to the reader.

Lemma 3: If $W$ is a submodule of $V$, and $\left< u, v \right>$ is a $G$ invariant
inner product, then $W^\perp = \{ v \in V: \left< w, v \right> = 0 \}$ is
also a submodule and $V = W \oplus W^\perp$.

(Proof of Lemma 3): Since $W$ is a subspace (as a vector space) then it is always the
case that $V = W \oplus W^\perp$. This is a result that is known from linear algebra.
Roughly the proof goes, let $\{ e_1, e_2, \ldots, e_k \}$ be an orthonormal basis of
$W$ (and you need to know that we can construct this), then for $v \in V$, let
$$w = \left< v, e_1 \right> e_1+ \left< v, e_2 \right> e_2+ \cdots + \left< v, e_k \right> e_k$$
then $v = w + (vw)$ and $w \in W$ and $vw \in W^\perp$.
$W^\perp$ is a submodule because if $v \in W^\perp$ then for all $w \in W$,
it will be the case that $g^{1} w \in W$ and so
$$\left< g v, w \right> = \left< g^{1} g v, g^{1} w \right> = \left< v, g^{1} w \right> = 0$$
and hence $gv \in W^\perp$.

(Proof of Machke's Theorem) If $V$ is irreducible, then the conclusion of Machke's theorem holds since $V$ itself is a direct sum of irreducible modules. So assume that $V$ is not irreducible, then there exists a proper submodule $W$ (that is, $W$ is not the $0$ module and it is not $V$ itself). By Lemma 1 and 2 there is a $G$ invariant scalar product, and by Lemma 3 $W^\perp$ is a submodule of $V$ as well and $V = W \oplus W^\perp$. Now since both $W$ and $W^\perp$ are of dimension smaller than $V$, we can assume that $W = W_1 \oplus \cdots \oplus W_\ell$ and $W^\perp = W_{\ell + 1} \oplus \cdots \oplus W_k$ for some $\ell$ and $k$ and irreducible submodules $W_i$ and hence $V = W_1 \oplus W_2 \oplus \cdots \oplus W_k$. 