begin
Lm1:
for R being non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr
for a being Element of R holds a * (0. R) = 0. R
begin
begin
begin
Lm2:
for F being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr
for x being Element of F holds (0. F) * x = 0. F
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 L 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 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 L holds eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (eval ((Leading-Monomial p),x)) * (eval ((Leading-Monomial q),x))
begin