---

Definition: oal_fabmon
oal_fabmon(s) ==  fabmon_of_nat_mcp(oal_omcp{s,<ℤ+>})

Lemma: oal_fabmon_wf
∀s:LOSet. (oal_fabmon(s) ∈ FAbMon(s))

Definition: oal_polyalg
oal_polyalg(s;a) ==  <oal_fabmon(s), omral_fma(oal_fabmon(s).mon;a)>

Lemma: oal_polyalg_wf
∀s:LOSet. ∀a:CDRng.  (oal_polyalg(s;a) ∈ polynom_alg{i:l}(s;a))



Home Index