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