---

Step * 1 1 1 1 1 of Lemma mon_itop_txpose_invar


1. g : IAbMonoid
2. n : ℕ
3. E : ℕn ⟶ |g|
4. x : ℕ+n
⊢ ((E[x] * (Π 0 + 1 ≤ j < x. E[j])) * (E[0] * (Π x + 1 ≤ j < n. E[j])))
= ((E[0] * (Π 0 + 1 ≤ j < x. E[j])) * (E[x] * (Π x + 1 ≤ j < n. E[j])))
∈ |g|
BY
{ (RW AbMonNormC 0 THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  IAbMonoid
2.  n  :  \mBbbN{}
3.  E  :  \mBbbN{}n  {}\mrightarrow{}  |g|
4.  x  :  \mBbbN{}\msupplus{}n
\mvdash{}  ((E[x]  *  (\mPi{}  0  +  1  \mleq{}  j  <  x.  E[j]))  *  (E[0]  *  (\mPi{}  x  +  1  \mleq{}  j  <  n.  E[j])))
=  ((E[0]  *  (\mPi{}  0  +  1  \mleq{}  j  <  x.  E[j]))  *  (E[x]  *  (\mPi{}  x  +  1  \mleq{}  j  <  n.  E[j])))


By

---

Latex:
(RW  AbMonNormC  0  THEN  Auto)

---

Home Index