---

Step * of Lemma alg_from_rng_wf

∀A:Type. ∀r:RngSig. ∀act:A ⟶ |r| ⟶ |r|.  (alg_from_rng(A;r;act) ∈ algebra_sig{i:l}(A))
BY
{ ((Unfolds ``alg_from_rng algebra_sig`` 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}A:Type.  \mforall{}r:RngSig.  \mforall{}act:A  {}\mrightarrow{}  |r|  {}\mrightarrow{}  |r|.    (alg\_from\_rng(A;r;act)  \mmember{}  algebra\_sig\{i:l\}(A))


By

---

Latex:
((Unfolds  ``alg\_from\_rng  algebra\_sig``  0)  THEN  Auto)

---

Home Index