environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, FINSEQ_1, SUBSET_1, XXREAL_0, RELAT_1, ARYTM_1, ORDINAL4, FUNCT_1, RFINSEQ, ALGSTR_1, ALGSTR_0, VECTSP_1, SUPINF_2, ARYTM_3, VECTSP_2, BINOP_1, MESFUNC1, STRUCT_0, RLVECT_1, LATTICES, GROUP_1, ZFMISC_1, NAT_1, POLYNOM3, CARD_3, CARD_1, ALGSEQ_1, POLYNOM1, TARSKI, PARTFUN1, FUNCT_4, POLYNOM2, FINSEQ_2, MSSUBFAM, QUOFIELD, POLYNOM4;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, FINSEQ_1, NAT_1, STRUCT_0, ALGSTR_0, FINSEQ_2, FUNCT_7, RFINSEQ, NAT_D, RLVECT_1, VFUNCT_1, GROUP_1, VECTSP_1, VECTSP_2, NORMSP_1, FVSUM_1, ALGSTR_1, GRCAT_1, QUOFIELD, ALGSEQ_1, POLYNOM3, GROUP_6, XXREAL_0;
definitions ALGSEQ_1, QUOFIELD, GROUP_1, VECTSP_1, GROUP_6;
theorems NAT_1, FUNCT_2, FUNCT_7, FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSEQ_5, RFINSEQ, RLVECT_1, VECTSP_1, VECTSP_2, FVSUM_1, NORMSP_1, ALGSEQ_1, GROUP_1, POLYNOM2, POLYNOM3, INT_1, NAT_2, MATRIX_3, ALGSTR_1, XREAL_1, XXREAL_0, BHSP_1, PARTFUN1, ORDINAL1, ALGSTR_0, XREAL_0, CARD_1;
schemes NAT_1, FINSEQ_2, POLYNOM3, FUNCT_2;
registrations ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1, FINSEQ_2, STRUCT_0, VECTSP_1, ALGSTR_1, POLYNOM3, ALGSTR_0, CARD_1, VFUNCT_1, FUNCT_2, RINGCAT1;
constructors HIDDEN, FINSEQOP, RFINSEQ, NAT_D, ALGSEQ_1, GRCAT_1, GROUP_6, QUOFIELD, POLYNOM3, REAL_1, ALGSTR_1, RELSET_1, FUNCT_7, FVSUM_1, VFUNCT_1, RINGCAT1;
requirements HIDDEN, NUMERALS, SUBSET, REAL, BOOLE, ARITHM;
equalities POLYNOM3, FINSEQ_2;
expansions ALGSEQ_1, QUOFIELD, VECTSP_1;
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
Lm2:
for L being non empty right_complementable add-associative right_zeroed distributive unital associative 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)))
Lm3:
for L being non trivial right_complementable add-associative right_zeroed distributive left_unital associative commutative 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))