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