---

Step * of Lemma lookup_omral_times_a

∀g:OCMon. ∀r:CDRng. ∀ps,qs:|omral(g;r)|. ∀z:|g|.
  (((ps ** qs)[z]) = (Σx ∈ dom(ps). Σy ∈ dom(qs). (when (x * y) =b z. ((ps[x]) * (qs[y])))) ∈ |r|)
BY
{ Unfold `rng_mssum` 0 THEN Lemma `lookup_omral_times` }

---

Latex:

---

Latex:
\mforall{}g:OCMon.  \mforall{}r:CDRng.  \mforall{}ps,qs:|omral(g;r)|.  \mforall{}z:|g|.
    (((ps  **  qs)[z])  =  (\mSigma{}x  \mmember{}  dom(ps).  \mSigma{}y  \mmember{}  dom(qs).  (when  (x  *  y)  =\msubb{}  z.  ((ps[x])  *  (qs[y])))))


By

---

Latex:
Unfold  `rng\_mssum`  0  THEN  Lemma  `lookup\_omral\_times`

---

Home Index