Step * of Lemma fma_alg_wf

G:GrpSig. ∀A:RngSig. ∀f:fma_sig{i:l}(G;A).  (f.alg ∈ algebra_sig{i:l}(|A|))
BY
ModulePiTac ``fma_alg fma_inj fma_umap`` }


Latex:


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


By


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




Home Index