begin
:: deftheorem POLYNOM7:def 1 :
canceled;
:: deftheorem Def2 defines non-zero POLYNOM7:def 2 :
for X being set
for R being non empty ZeroStr
for p being Series of X,R holds
( p is non-zero iff p <> 0_ X,R );
theorem Th1:
theorem
:: deftheorem Def3 defines univariate POLYNOM7:def 3 :
for X being set
for b being bag of X holds
( b is univariate iff ex u being Element of X st support b = {u} );
begin
theorem
Lm1:
for L being non empty doubleLoopStr
for p being Polynomial of {} ,L ex a being Element of L st p = {(EmptyBag {} )} --> a
theorem
theorem
begin
:: deftheorem Def4 defines monomial-like POLYNOM7:def 4 :
for X being set
for L being non empty ZeroStr
for p being Series of X,L holds
( p is monomial-like iff ex b being bag of X st
for b9 being bag of X st b9 <> b holds
p . b9 = 0. L );
theorem Th6:
:: deftheorem defines Monom POLYNOM7:def 5 :
for X being set
for L being non empty ZeroStr
for a being Element of L
for b being bag of X holds Monom a,b = (0_ X,L) +* b,a;
:: deftheorem Def6 defines term POLYNOM7:def 6 :
for X being set
for L being non empty ZeroStr
for m being Monomial of X,L
for b4 being bag of X holds
( b4 = term m iff ( m . b4 <> 0. L or ( Support m = {} & b4 = EmptyBag X ) ) );
:: deftheorem defines coefficient POLYNOM7:def 7 :
for X being set
for L being non empty ZeroStr
for m being Monomial of X,L holds coefficient m = m . (term m);
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem
begin
:: deftheorem Def8 defines Constant POLYNOM7:def 8 :
for X being set
for L being non empty ZeroStr
for p being Series of X,L holds
( p is Constant iff for b being bag of X st b <> EmptyBag X holds
p . b = 0. L );
theorem Th14:
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) )
theorem Th15:
theorem
:: deftheorem defines | POLYNOM7:def 9 :
for X being set
for L being non empty ZeroStr
for a being Element of L holds a | X,L = (0_ X,L) +* (EmptyBag X),a;
Lm3:
for X being set
for L being non empty ZeroStr holds (0. L) | X,L = 0_ X,L
theorem
theorem Th18:
theorem
theorem
theorem
theorem
theorem Th23:
theorem Th24:
theorem Th25:
begin
:: deftheorem Def10 defines * POLYNOM7:def 10 :
for X being set
for L being non empty multLoopStr_0
for p being Series of X,L
for a being Element of L
for b5 being Series of X,L holds
( b5 = a * p iff for b being bag of X holds b5 . b = a * (p . b) );
:: deftheorem Def11 defines * POLYNOM7:def 11 :
for X being set
for L being non empty multLoopStr_0
for p being Series of X,L
for a being Element of L
for b5 being Series of X,L holds
( b5 = p * a iff for b being bag of X holds b5 . b = (p . b) * a );
theorem
theorem Th27:
theorem Th28:
Lm4:
for n being Ordinal
for L being non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive 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 associative commutative well-unital distributive 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
theorem
theorem
theorem
theorem
theorem
theorem