Step
*
of Lemma
algebra_hom_properties
∀A:RngSig. ∀M,N:algebra_sig{i:l}(|A|). ∀f:algebra_hom(A; M; N).
  (FunThru2op(M.car;N.car;M.times;N.times;f) ∧ ((f M.one) = N.one ∈ N.car))
BY
{ ProvePropertiesLemma }
Latex:
Latex:
\mforall{}A:RngSig.  \mforall{}M,N:algebra\_sig\{i:l\}(|A|).  \mforall{}f:algebra\_hom(A;  M;  N).
    (FunThru2op(M.car;N.car;M.times;N.times;f)  \mwedge{}  ((f  M.one)  =  N.one))
By
Latex:
ProvePropertiesLemma
Home
Index