environ
vocabularies HIDDEN, RLVECT_1, ALGSTR_1, ALGSTR_0, VECTSP_1, BINOP_1, LATTICES, VECTSP_2, ZFMISC_1, XBOOLE_0, STRUCT_0, POLYNOM1, VALUED_0, SUBSET_1, SUPINF_2, FUNCT_4, PRE_POLY, FUNCT_1, FUNCOP_1, RELAT_1, ORDINAL1, CARD_1, PARTFUN1, POLYNOM2, FINSEQ_1, CARD_3, NUMBERS, XXREAL_0, FINSET_1, ORDERS_1, ARYTM_3, NAT_1, MESFUNC1, QUOFIELD, GROUP_1, TARSKI, MSSUBFAM, ALGSEQ_1, CAT_3, XCMPLX_0, ORDINAL4, POLYNOM7, FUNCT_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, FUNCT_1, FINSET_1, ORDINAL1, PARTFUN1, FUNCT_2, FUNCT_7, POLYNOM1, NUMBERS, XXREAL_0, DOMAIN_1, STRUCT_0, ALGSTR_0, FUNCT_4, NAT_1, ALGSTR_1, RLVECT_1, ORDERS_1, FINSEQ_1, FUNCOP_1, GROUP_1, QUOFIELD, GRCAT_1, VECTSP_2, POLYNOM2, VECTSP_1, GROUP_6, PRE_POLY;
definitions ;
theorems TARSKI, FINSEQ_1, FUNCT_1, FUNCT_2, RELAT_1, ZFMISC_1, VECTSP_1, POLYNOM1, QUOFIELD, FUNCT_7, FUNCT_4, FUNCOP_1, BINOM, FINSEQ_3, RLVECT_1, VECTSP_2, GROUP_1, NAT_1, FINSEQ_2, FINSEQ_5, MATRLIN, POLYNOM2, XBOOLE_0, XREAL_1, GROUP_6, XXREAL_0, ORDINAL1, PARTFUN1, PRE_POLY, XTUPLE_0, PBOOLE;
schemes FUNCT_2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCOP_1, FINSET_1, XREAL_0, STRUCT_0, VECTSP_1, ALGSTR_1, POLYNOM1, POLYNOM2, ALGSTR_0, CARD_1, SUBSET_1, PRE_POLY, FUNCT_1, RINGCAT1, MOD_4;
constructors HIDDEN, REALSET2, GRCAT_1, GROUP_6, TRIANG_1, QUOFIELD, POLYNOM2, ALGSTR_1, RELSET_1, FUNCT_7, FVSUM_1, FUNCT_4, RINGCAT1, MOD_4;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities FUNCOP_1, STRUCT_0, ORDINAL1;
expansions FUNCT_2, STRUCT_0, RINGCAT1, MOD_4;
definition
let X be
set ;
let b be
bag of
X;
end;
Lm1:
for L being non empty doubleLoopStr
for p being Polynomial of {},L ex a being Element of L st p = {(EmptyBag {})} --> a
Lm2:
for X being set
for L being non empty ZeroStr
for c being ConstPoly of X,L holds
( term c = EmptyBag X & coefficient c = c . (EmptyBag X) )
Lm3:
for X being set
for L being non empty ZeroStr holds (0. L) | (X,L) = 0_ (X,L)
Lm4:
for n being Ordinal
for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative left_zeroed doubleLoopStr
for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval (((a | (n,L)) *' p),x) = a * (eval (p,x))
Lm5:
for n being Ordinal
for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative left_zeroed doubleLoopStr
for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval ((p *' (a | (n,L))),x) = (eval (p,x)) * a