---

Step * of Lemma module_hom_plus

∀[A:RngSig]. ∀[M,N:algebra_sig{i:l}(|A|)]. ∀[f:module_hom(A; M; N)]. ∀[a1,a2:M.car].
  ((f (a1 M.plus a2)) = ((f a1) N.plus (f a2)) ∈ N.car)
BY
{ ((ProvePropertyLemma `fun_thru_2op` 4) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:RngSig].  \mforall{}[M,N:algebra\_sig\{i:l\}(|A|)].  \mforall{}[f:module\_hom(A;  M;  N)].  \mforall{}[a1,a2:M.car].
    ((f  (a1  M.plus  a2))  =  ((f  a1)  N.plus  (f  a2)))


By

---

Latex:
((ProvePropertyLemma  `fun\_thru\_2op`  4)  THEN  Auto)

---

Home Index