---

Step * of Lemma omral_alg_umap_tri_comm

∀g:OCMon. ∀a:CDRng. ∀n:algebra{i:l}(a). ∀f:|g| ⟶ n.car.  ((alg_umap(n,f) o (λk.inj(k,1))) = f ∈ (|g| ⟶ n.car))
BY
{ ((RepD THENM New [`k1'] Ext 
THENM Eval ``omral_alg_umap`` 0) THENA Auto) }

1
1. g : OCMon
2. a : CDRng
3. n : algebra{i:l}(a)
4. f : |g| ⟶ n.car
5. k1 : |g|
⊢ (Σk ∈ dom(inj(k1,1)). ((inj(k1,1)[k]) n.act (f k))) = (f k1) ∈ n.car

---

Latex:

---

Latex:
\mforall{}g:OCMon.  \mforall{}a:CDRng.  \mforall{}n:algebra\{i:l\}(a).  \mforall{}f:|g|  {}\mrightarrow{}  n.car.    ((alg\_umap(n,f)  o  (\mlambda{}k.inj(k,1)))  =  f)


By

---

Latex:
((RepD  THENM  New  [`k1']  Ext 
THENM  Eval  ``omral\_alg\_umap``  0)  THENA  Auto)

---

Home Index