environ
vocabularies HIDDEN, NUMBERS, RLVECT_1, ALGSTR_0, XBOOLE_0, FINSEQ_1, STRUCT_0, SUBSET_1, RELAT_1, FUNCT_1, SUPINF_2, CARD_3, NAT_1, PARTFUN1, FINSEQ_5, ORDINAL4, ARYTM_3, XXREAL_0, FINSEQ_3, FINSEQ_2, PRE_POLY, TARSKI, CARD_1, ORDERS_1, RELAT_2, FINSET_1, ARYTM_1, FUNCT_2, POLYNOM1, ALGSEQ_1, FUNCOP_1, FUNCT_4, MESFUNC1, LATTICES, VECTSP_1, BINOP_1, CLASSES1, GROUP_1, ZFMISC_1, POLYNOM3, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, RELAT_1, RELAT_2, FUNCT_1, ORDERS_1, XXREAL_0, XREAL_0, NAT_1, NAT_D, CLASSES1, RELSET_1, PARTFUN1, FINSET_1, FUNCT_2, FUNCOP_1, FINSEQ_1, PRE_POLY, FINSEQ_2, FINSEQ_5, BINOP_1, RVSUM_1, FUNCT_7, TREES_4, VALUED_0, WSIERP_1, MATRIX_0, STRUCT_0, ALGSTR_0, MATRLIN, GROUP_1, RLVECT_1, VFUNCT_1, FVSUM_1, VECTSP_1, NORMSP_1, POLYNOM1, ALGSEQ_1, RECDEF_1;
definitions TARSKI, XBOOLE_0, RELAT_1, RELAT_2, RLVECT_1, GROUP_1, VECTSP_1, ALGSEQ_1, FUNCT_2, ALGSTR_0;
theorems AXIOMS, TARSKI, ENUMSET1, RELSET_1, INT_1, NAT_1, CARD_1, RLVECT_1, VECTSP_1, ALGSEQ_1, RELAT_2, ORDERS_1, FUNCT_1, FUNCT_2, FUNCT_7, FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSEQ_5, RFINSEQ, BINOP_1, CARD_3, RVSUM_1, FVSUM_1, MATRLIN, POLYNOM1, RELAT_1, XBOOLE_0, RLVECT_2, XCMPLX_1, PARTFUN1, GROUP_1, XREAL_1, XXREAL_0, ORDINAL1, BHSP_1, NORMSP_1, XREAL_0, NAT_D, PRE_POLY, NUMBERS;
schemes FUNCT_2, FINSEQ_1, FINSEQ_2, NAT_1, RELSET_1, SUBSET_1, BINOP_1, RECDEF_1;
registrations ORDINAL1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, FINSEQ_2, FINSEQ_5, STRUCT_0, VECTSP_1, VALUED_0, FINSET_1, RELSET_1, PRE_POLY, VFUNCT_1, CARD_1, FUNCT_1, FINSEQ_3, XCMPLX_0, RVSUM_1;
constructors HIDDEN, BINOP_1, FINSEQOP, REALSET1, NAT_D, FINSEQ_5, WSIERP_1, ALGSEQ_1, TRIANG_1, POLYNOM1, RECDEF_1, BINARITH, CLASSES1, RELSET_1, FUNCT_7, MATRLIN, FVSUM_1, VFUNCT_1, NUMBERS;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities XBOOLE_0, FINSEQ_2, STRUCT_0, ALGSTR_0;
expansions RELAT_2, VECTSP_1, ALGSEQ_1, FUNCT_2;
Lm1:
for L being non empty addLoopStr
for p, q being sequence of L holds p - q = p + (- q)
definition
let L be non
empty right_complementable add-associative right_zeroed distributive doubleLoopStr ;
existence
ex b1 being non empty strict doubleLoopStr st
( ( for x being set holds
( x in the carrier of b1 iff x is Polynomial of L ) ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. b1 = 0_. L & 1. b1 = 1_. L )
uniqueness
for b1, b2 being non empty strict doubleLoopStr st ( for x being set holds
( x in the carrier of b1 iff x is Polynomial of L ) ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. b1 = 0_. L & 1. b1 = 1_. L & ( for x being set holds
( x in the carrier of b2 iff x is Polynomial of L ) ) & ( for x, y being Element of b2
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b2
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. b2 = 0_. L & 1. b2 = 1_. L holds
b1 = b2
end;