environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, SUBSET_1, FINSEQ_1, RELAT_1, PARTFUN1, CARD_1, FUNCT_1, TARSKI, XXREAL_0, ARYTM_1, ARYTM_3, NAT_1, ORDERS_1, RELAT_2, GROUP_1, BINOP_1, ALGSTR_0, RLVECT_1, VECTSP_1, LATTICES, ZFMISC_1, FINSET_1, ALGSTR_1, STRUCT_0, SUPINF_2, CARD_3, FINSOP_1, ORDINAL4, PRE_POLY, FINSEQ_5, FUNCT_4, FUNCOP_1, ORDINAL1, WELLORD2, MESFUNC1, RFINSEQ, POLYNOM1, ALGSEQ_1, MSSUBFAM, QUOFIELD, POLYNOM2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, RELAT_1, FINSOP_1, RELAT_2, RELSET_1, FUNCT_1, FINSET_1, XCMPLX_0, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_4, FUNCT_7, REAL_1, NAT_1, ALGSTR_1, ORDERS_1, FINSEQ_1, STRUCT_0, ALGSTR_0, RLVECT_1, FUNCOP_1, VFUNCT_1, VECTSP_1, GROUP_1, GROUP_4, QUOFIELD, FINSEQ_5, GRCAT_1, RFINSEQ, YELLOW_1, GROUP_6, XXREAL_0, RECDEF_1, PRE_POLY, POLYNOM1;
definitions QUOFIELD, GROUP_1;
theorems TARSKI, FINSEQ_1, FUNCT_1, FUNCT_2, ORDINAL1, RELAT_1, ZFMISC_1, VECTSP_1, POLYNOM1, RELAT_2, FUNCT_7, FUNCT_4, FUNCOP_1, ORDERS_1, NAT_1, FINSEQ_4, INT_1, FINSEQ_3, RLVECT_1, GROUP_4, PARTFUN2, CARD_1, RFINSEQ, FINSOP_1, FINSEQ_5, CARD_2, FINSEQ_2, ALGSTR_1, GROUP_1, XBOOLE_0, XBOOLE_1, PARTFUN1, XREAL_1, GROUP_6, XXREAL_0, PRE_POLY, XTUPLE_0;
schemes FUNCT_2, NAT_1, RECDEF_1, INT_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCOP_1, FINSET_1, XREAL_0, NAT_1, INT_1, FINSEQ_1, STRUCT_0, VECTSP_1, ALGSTR_1, MONOID_0, POLYNOM1, VALUED_0, CARD_1, SUBSET_1, PRE_POLY, RELAT_1, VFUNCT_1, FUNCT_2, FUNCT_1, PBOOLE, RINGCAT1;
constructors HIDDEN, REAL_1, FINSOP_1, RFINSEQ, BINARITH, FINSEQ_5, GROUP_4, GRCAT_1, GROUP_6, MONOID_0, TRIANG_1, YELLOW_1, QUOFIELD, POLYNOM1, RECDEF_1, ALGSTR_1, RELSET_1, FUNCT_7, FVSUM_1, VFUNCT_1, DOMAIN_1, RINGCAT1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities BINOP_1, FUNCOP_1, ALGSTR_0;
expansions QUOFIELD;
Lm1:
for X being set
for A being Subset of X
for O being Order of X holds
( O is_reflexive_in A & O is_antisymmetric_in A & O is_transitive_in A )
Lm2:
for X being set
for A being Subset of X
for O being Order of X st O is_connected_in X holds
O is_connected_in A
Lm3:
for X being set
for S being Subset of X
for R being Order of X st R is being_linear-order holds
R linearly_orders S
definition
let n be
Ordinal;
let b be
bag of
n;
let L be non
trivial well-unital doubleLoopStr ;
let x be
Function of
n,
L;
existence
ex b1 being Element of L ex y being FinSequence of the carrier of L st
( len y = len (SgmX ((RelIncl n),(support b))) & b1 = Product y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = (power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i)) ) )
uniqueness
for b1, b2 being Element of L st ex y being FinSequence of the carrier of L st
( len y = len (SgmX ((RelIncl n),(support b))) & b1 = Product y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = (power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i)) ) ) & ex y being FinSequence of the carrier of L st
( len y = len (SgmX ((RelIncl n),(support b))) & b2 = Product y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = (power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i)) ) ) holds
b1 = b2
end;
Lm4:
for n being Ordinal
for L being non empty non trivial right_complementable associative commutative add-associative right_zeroed well-unital distributive doubleLoopStr
for b1, b2 being bag of n
for u being object st not u in support b1 & support b2 = (support b1) \/ {u} & ( for u9 being object st u9 <> u holds
b2 . u9 = b1 . u9 ) holds
for x being Function of n,L
for a being Element of L st a = (power L) . ((x . u),(b2 . u)) holds
eval (b2,x) = a * (eval (b1,x))
Lm5:
for n being Ordinal
for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for b1 being bag of n st ex u being set st support b1 = {u} holds
for b2 being bag of n
for x being Function of n,L holds eval ((b1 + b2),x) = (eval (b1,x)) * (eval (b2,x))
definition
let n be
Ordinal;
let L be non
trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ;
let p be
Polynomial of
n,
L;
let x be
Function of
n,
L;
existence
ex b1 being Element of L ex y being FinSequence of the carrier of L st
( len y = len (SgmX ((BagOrder n),(Support p))) & b1 = Sum y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((p * (SgmX ((BagOrder n),(Support p)))) /. i) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) ) )
uniqueness
for b1, b2 being Element of L st ex y being FinSequence of the carrier of L st
( len y = len (SgmX ((BagOrder n),(Support p))) & b1 = Sum y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((p * (SgmX ((BagOrder n),(Support p)))) /. i) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) ) ) & ex y being FinSequence of the carrier of L st
( len y = len (SgmX ((BagOrder n),(Support p))) & b2 = Sum y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((p * (SgmX ((BagOrder n),(Support p)))) /. i) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) ) ) holds
b1 = b2
end;
Lm6:
for n being Ordinal
for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p, q being Polynomial of n,L
for x being Function of n,L
for b being bag of n st not b in Support p & Support q = (Support p) \/ {b} & ( for b9 being bag of n st b9 <> b holds
q . b9 = p . b9 ) holds
eval (q,x) = (eval (p,x)) + ((q . b) * (eval (b,x)))
Lm7:
for n being Ordinal
for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of n,L st ex b being bag of n st Support p = {b} holds
for q being Polynomial of n,L
for x being Function of n,L holds eval ((p + q),x) = (eval (p,x)) + (eval (q,x))
Lm8:
for n being Ordinal
for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p, q being Polynomial of n,L
for b1, b2 being bag of n st Support p = {b1} & Support q = {b2} holds
for x being Function of n,L holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))
Lm9:
for n being Ordinal
for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for q being Polynomial of n,L st ex b being bag of n st Support q = {b} holds
for p being Polynomial of n,L
for x being Function of n,L holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))
definition
let n be
Ordinal;
let L be non
trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ;
let x be
Function of
n,
L;
existence
ex b1 being Function of (Polynom-Ring (n,L)),L st
for p being Polynomial of n,L holds b1 . p = eval (p,x)
uniqueness
for b1, b2 being Function of (Polynom-Ring (n,L)),L st ( for p being Polynomial of n,L holds b1 . p = eval (p,x) ) & ( for p being Polynomial of n,L holds b2 . p = eval (p,x) ) holds
b1 = b2
end;