begin
theorem
canceled;
theorem
canceled;
theorem
Lm1:
for R being non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr
for a being Element of holds a * (0. R) = 0. R
begin
theorem
canceled;
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem
theorem
begin
:: deftheorem Def1 defines Leading-Monomial POLYNOM4:def 1 :
theorem Th14:
theorem Th15:
theorem
theorem
theorem Th18:
theorem Th19:
begin
:: deftheorem Def2 defines eval POLYNOM4:def 2 :
theorem Th20:
theorem Th21:
Lm2:
for F being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr
for x being Element of holds (0. F) * x = 0. F
theorem Th22:
theorem Th23:
theorem
theorem Th25:
Lm3:
for L being non empty right_complementable add-associative right_zeroed unital associative distributive doubleLoopStr
for p, q being Polynomial of L st len p > 0 & len q > 0 holds
for x being Element of holds eval ((Leading-Monomial p) *' (Leading-Monomial q)),x = ((p . ((len p) -' 1)) * (q . ((len q) -' 1))) * ((power L) . x,(((len p) + (len q)) -' 2))
Lm4:
for L being non empty non trivial right_complementable add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr
for p, q being Polynomial of L
for x being Element of holds eval ((Leading-Monomial p) *' (Leading-Monomial q)),x = (eval (Leading-Monomial p),x) * (eval (Leading-Monomial q),x)
theorem Th26:
theorem Th27:
begin
:: deftheorem Def3 defines Polynom-Evaluation POLYNOM4:def 3 :