---

Step * of Lemma rP_to_term-int_term_to_rP

∀[t:int_term()]. ∀[s:int_term() List].  (rP_to_term(s;int_term_to_rP(t)) ~ [t / s])
BY
{ Assert ⌜(int_term() ⊆r Base) ∧ ((iPolynomial() List) ⊆r Base)⌝⋅ }

1
.....assertion..... 
(int_term() ⊆r Base) ∧ ((iPolynomial() List) ⊆r Base)

2
1. (int_term() ⊆r Base) ∧ ((iPolynomial() List) ⊆r Base)
⊢ ∀[t:int_term()]. ∀[s:int_term() List].  (rP_to_term(s;int_term_to_rP(t)) ~ [t / s])

---

Latex:

---

Latex:
\mforall{}[t:int\_term()].  \mforall{}[s:int\_term()  List].    (rP\_to\_term(s;int\_term\_to\_rP(t))  \msim{}  [t  /  s])


By

---

Latex:
Assert  \mkleeneopen{}(int\_term()  \msubseteq{}r  Base)  \mwedge{}  ((iPolynomial()  List)  \msubseteq{}r  Base)\mkleeneclose{}\mcdot{}

---

Home Index