---

Step * of Lemma mon_reduce_functionality_wrt_permr

∀g:IAbMonoid. ∀xs,ys:|g| List.  ((xs ≡(|g|) ys) ⇒ ((Π xs) = (Π ys) ∈ |g|))
BY
{ Auto }

1
1. g : IAbMonoid
2. xs : |g| List
3. ys : |g| List
4. xs ≡(|g|) ys
⊢ (Π xs) = (Π ys) ∈ |g|

---

Latex:

---

Latex:
\mforall{}g:IAbMonoid.  \mforall{}xs,ys:|g|  List.    ((xs  \mequiv{}(|g|)  ys)  {}\mRightarrow{}  ((\mPi{}  xs)  =  (\mPi{}  ys)))


By

---

Latex:
Auto

---

Home Index