---

Step * of Lemma fma_umap_wf

∀G:GrpSig. ∀A:RngSig. ∀f:fma_sig{i:l}(G;A).  (f.umap ∈ N:algebra{i:l}(A) ⟶ (|G| ⟶ N.car) ⟶ f.alg.car ⟶ N.car)
BY
{ ModulePiTac 3 ``fma_alg fma_inj fma_umap`` }

---

Latex:

---

Latex:
\mforall{}G:GrpSig.  \mforall{}A:RngSig.  \mforall{}f:fma\_sig\{i:l\}(G;A).
    (f.umap  \mmember{}  N:algebra\{i:l\}(A)  {}\mrightarrow{}  (|G|  {}\mrightarrow{}  N.car)  {}\mrightarrow{}  f.alg.car  {}\mrightarrow{}  N.car)


By

---

Latex:
ModulePiTac  3  ``fma\_alg  fma\_inj  fma\_umap``

---

Home Index