:: POLYNOM7 semantic presentation

begin

registration
cluster non empty non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive domRing-like left_zeroed for doubleLoopStr ;
existence
 ex b1 being non trivial doubleLoopStr st
( b1 is Abelian & b1 is left_zeroed & b1 is right_zeroed & b1 is add-associative & b1 is right_complementable & b1 is well-unital & b1 is associative & b1 is commutative & b1 is distributive & b1 is domRing-like )
proof
set R = the domRing;
take  the domRing ; ::_thesis: ( the domRing is Abelian & the domRing is left_zeroed & the domRing is right_zeroed & the domRing is add-associative & the domRing is right_complementable & the domRing is well-unital & the domRing is associative & the domRing is commutative & the domRing is distributive & the domRing is domRing-like )
thus  ( the domRing is Abelian & the domRing is left_zeroed & the domRing is right_zeroed & the domRing is add-associative & the domRing is right_complementable & the domRing is well-unital & the domRing is associative & the domRing is commutative & the domRing is distributive & the domRing is domRing-like ) ; ::_thesis: verum
end;
end;

definition
let X be set ;
let R be non empty ZeroStr ;
let p be Series of X,R;
attrp is non-zero  means :Def1: :: POLYNOM7:def 1
p <> 0_ (X,R);
end;

:: deftheorem Def1 defines non-zero POLYNOM7:def_1_:_
 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) );

registration
let X be set ;
let R be non trivial ZeroStr ;
cluster Relation-like Bags X -defined the carrier of R -valued Function-like V18( Bags X, the carrier of R) non-zero for Element of bool [:(Bags X), the carrier of R:];
existence
 ex b1 being Series of X,R st b1 is non-zero
proof
set a = the Element of NonZero R;
A1: not the Element of NonZero R in {(0. R)} by XBOOLE_0:def_5;
reconsider a = the Element of NonZero R as Element of R ;
set p = (0_ (X,R)) +* ((EmptyBag X),a);
reconsider p = (0_ (X,R)) +* ((EmptyBag X),a) as Function of (Bags X), the carrier of R ;
reconsider p = p as Function of (Bags X),R ;
reconsider p = p as Series of X,R ;
take  p ; ::_thesis: p is non-zero
 0_ (X,R) = (Bags X) --> (0. R) by POLYNOM1:def_7;
then  dom (0_ (X,R)) = Bags X by FUNCOP_1:13;
then A2: p . (EmptyBag X) = a by FUNCT_7:31;
 a <> 0. R by A1, TARSKI:def_1;
then  p <> 0_ (X,R) by A2, POLYNOM1:22;
hence  p is non-zero by Def1; ::_thesis: verum
end;
end;

registration
let n be Ordinal;
let R be non trivial ZeroStr ;
cluster Relation-like Bags n -defined the carrier of R -valued Function-like V18( Bags n, the carrier of R) finite-Support non-zero for Element of bool [:(Bags n), the carrier of R:];
existence
 ex b1 being Polynomial of n,R st b1 is non-zero
proof
set a = the Element of NonZero R;
A1: not the Element of NonZero R in {(0. R)} by XBOOLE_0:def_5;
reconsider a = the Element of NonZero R as Element of R ;
set p = (0_ (n,R)) +* ((EmptyBag n),a);
reconsider p = (0_ (n,R)) +* ((EmptyBag n),a) as Function of (Bags n), the carrier of R ;
reconsider p = p as Function of (Bags n),R ;
reconsider p = p as Series of n,R ;
A2: now__::_thesis:_for_u_being_set_st_u_in_Support_p_holds_
u_in_{(EmptyBag_n)}
let u be set ; ::_thesis: ( u in Support p implies u in {(EmptyBag n)} )
assume A3: u in Support p ; ::_thesis: u in {(EmptyBag n)}
then  u is Element of Bags n ;
then A4: u is bag of n ;
now__::_thesis:_not_u_<>_EmptyBag_n
assume  u <> EmptyBag n ; ::_thesis: contradiction
then p . u = (0_ (n,R)) . u by FUNCT_7:32
.= 0. R by A4, POLYNOM1:22 ;
hence  contradiction by A3, POLYNOM1:def_3; ::_thesis: verum
end;
hence  u in {(EmptyBag n)} by TARSKI:def_1; ::_thesis: verum
end;
 0_ (n,R) = (Bags n) --> (0. R) by POLYNOM1:def_7;
then  dom (0_ (n,R)) = Bags n by FUNCOP_1:13;
then A5: p . (EmptyBag n) = a by FUNCT_7:31;
now__::_thesis:_for_u_being_set_st_u_in_{(EmptyBag_n)}_holds_
u_in_Support_p
let u be set ; ::_thesis: ( u in {(EmptyBag n)} implies u in Support p )
assume  u in {(EmptyBag n)} ; ::_thesis: u in Support p
then A6: u = EmptyBag n by TARSKI:def_1;
 a <> 0. R by A1, TARSKI:def_1;
hence  u in Support p by A5, A6, POLYNOM1:def_3; ::_thesis: verum
end;
then  Support p = {(EmptyBag n)} by A2, TARSKI:1;
then reconsider p = p as Polynomial of n,R by POLYNOM1:def_4;
take  p ; ::_thesis: p is non-zero
 a <> 0. R by A1, TARSKI:def_1;
then  p <> 0_ (n,R) by A5, POLYNOM1:22;
hence  p is non-zero by Def1; ::_thesis: verum
end;
end;

theorem Th1: :: POLYNOM7:1
for X being set
for R being non empty ZeroStr
for s being Series of X,R holds
( s = 0_ (X,R) iff Support s = {} )
proof
let X be set ; ::_thesis: for R being non empty ZeroStr
for s being Series of X,R holds
( s = 0_ (X,R) iff Support s = {} )
let R be non empty ZeroStr ; ::_thesis: for s being Series of X,R holds
( s = 0_ (X,R) iff Support s = {} )
let s be Series of X,R; ::_thesis: ( s = 0_ (X,R) iff Support s = {} )
A1: now__::_thesis:_(_Support_s_=_{}_implies_s_=_0__(X,R)_)
assume A2: Support s = {} ; ::_thesis: s = 0_ (X,R)
A3: now__::_thesis:_for_x_being_set_st_x_in_Bags_X_holds_
s_._x_=_(0__(X,R))_._x
let x be set ; ::_thesis: ( x in Bags X implies s . x = (0_ (X,R)) . x )
assume  x in Bags X ; ::_thesis: s . x = (0_ (X,R)) . x
then reconsider x9 = x as Element of Bags X ;
 s . x9 = 0. R by A2, POLYNOM1:def_3;
hence  s . x = (0_ (X,R)) . x by POLYNOM1:22; ::_thesis: verum
end;
 ( dom s = Bags X & dom (0_ (X,R)) = Bags X ) by FUNCT_2:def_1;
hence  s = 0_ (X,R) by A3, FUNCT_1:2; ::_thesis: verum
end;
now__::_thesis:_(_s_=_0__(X,R)_implies_Support_s_=_{}_)
assume A4: s = 0_ (X,R) ; ::_thesis: Support s = {}
now__::_thesis:_not_Support_s_<>_{}
set x = the Element of Support s;
assume  Support s <> {} ; ::_thesis: contradiction
then A5: the Element of Support s in Support s ;
then reconsider x = the Element of Support s as bag of X ;
 s . x <> 0. R by A5, POLYNOM1:def_3;
hence  contradiction by A4, POLYNOM1:22; ::_thesis: verum
end;
hence  Support s = {} ; ::_thesis: verum
end;
hence  ( s = 0_ (X,R) iff Support s = {} ) by A1; ::_thesis: verum
end;

theorem :: POLYNOM7:2
for X being set
for R being non empty ZeroStr holds
( not R is trivial iff ex s being Series of X,R st Support s <> {} )
proof
let X be set ; ::_thesis: for R being non empty ZeroStr holds
( not R is trivial iff ex s being Series of X,R st Support s <> {} )
let R be non empty ZeroStr ; ::_thesis: ( not R is trivial iff ex s being Series of X,R st Support s <> {} )
A1: now__::_thesis:_(_not_R_is_trivial_implies_ex_s,_s_being_Series_of_X,R_st_Support_s_<>_{}_)
set x = EmptyBag X;
assume A2: not R is trivial ; ::_thesis: ex s, s being Series of X,R st Support s <> {}
now__::_thesis:_ex_a_being_Element_of_R_st_a_<>_0._R
assume A3: for a being Element of R holds not a <> 0. R ; ::_thesis: contradiction
 ex x being set st the carrier of R = {x}
proof
take  0. R ; ::_thesis: the carrier of R = {(0. R)}
A4: now__::_thesis:_for_u_being_set_st_u_in_the_carrier_of_R_holds_
u_in_{(0._R)}
let u be set ; ::_thesis: ( u in the carrier of R implies u in {(0. R)} )
assume  u in the carrier of R ; ::_thesis: u in {(0. R)}
then  u = 0. R by A3;
hence  u in {(0. R)} by TARSKI:def_1; ::_thesis: verum
end;
 for u being set st u in {(0. R)} holds
u in the carrier of R ;
hence  the carrier of R = {(0. R)} by A4, TARSKI:1; ::_thesis: verum
end;
hence  contradiction by A2; ::_thesis: verum
end;
then consider a being Element of R such that
A5: a <> 0. R ;
set s = (Bags X) --> a;
reconsider s = (Bags X) --> a as Function of (Bags X), the carrier of R ;
reconsider s = s as Function of (Bags X),R ;
reconsider s = s as Series of X,R ;
take s = s; ::_thesis: ex s being Series of X,R st Support s <> {}
 s . (EmptyBag X) = a by FUNCOP_1:7;
then  EmptyBag X in Support s by A5, POLYNOM1:def_3;
hence  ex s being Series of X,R st Support s <> {} ; ::_thesis: verum
end;
now__::_thesis:_(_ex_s_being_Series_of_X,R_st_Support_s_<>_{}_implies_not_R_is_trivial_)
assume  ex s being Series of X,R st Support s <> {} ; ::_thesis: not R is trivial
then consider s being Series of X,R such that
A6: Support s <> {} ;
set b = the Element of Support s;
 the Element of Support s in Support s by A6;
then reconsider b = the Element of Support s as Element of Bags X ;
now__::_thesis:_for_x_being_set_holds_not_the_carrier_of_R_=_{x}
assume  ex x being set st the carrier of R = {x} ; ::_thesis: contradiction
then consider x being set  such that
A7: the carrier of R = {x} ;
0. R = x by A7, TARSKI:def_1
.= s . b by A7, TARSKI:def_1 ;
hence  contradiction by A6, POLYNOM1:def_3; ::_thesis: verum
end;
hence  not R is trivial by ZFMISC_1:131; ::_thesis: verum
end;
hence  ( not R is trivial iff ex s being Series of X,R st Support s <> {} ) by A1; ::_thesis: verum
end;

definition
let X be set ;
let b be bag of X;
attrb is univariate  means :Def2: :: POLYNOM7:def 2
 ex u being Element of X st support b = {u};
end;

:: deftheorem Def2 defines univariate POLYNOM7:def_2_:_
 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} );

registration
let X be non empty set ;
cluster Relation-like X -defined Function-like total V208() finite-support univariate for set ;
existence
 ex b1 being bag of X st b1 is univariate
proof
set x = the Element of X;
set b = (EmptyBag X) +* ( the Element of X,1);
take  (EmptyBag X) +* ( the Element of X,1) ; ::_thesis: (EmptyBag X) +* ( the Element of X,1) is univariate
A1: dom (EmptyBag X) = X by PARTFUN1:def_2;
then A2: ((EmptyBag X) +* ( the Element of X,1)) . the Element of X = ((EmptyBag X) +* ( the Element of X .--> 1)) . the Element of X by FUNCT_7:def_3;
A3: dom ( the Element of X .--> 1) = { the Element of X} by FUNCOP_1:13;
A4: for u being set st u in support ((EmptyBag X) +* ( the Element of X,1)) holds
u in { the Element of X}
proof
let u be set ; ::_thesis: ( u in support ((EmptyBag X) +* ( the Element of X,1)) implies u in { the Element of X} )
assume A5: u in support ((EmptyBag X) +* ( the Element of X,1)) ; ::_thesis: u in { the Element of X}
now__::_thesis:_not_u_<>_the_Element_of_X
assume  u <> the Element of X ; ::_thesis: contradiction
then A6: not u in dom ( the Element of X .--> 1) by A3, TARSKI:def_1;
 ((EmptyBag X) +* ( the Element of X,1)) . u = ((EmptyBag X) +* ( the Element of X .--> 1)) . u by A1, FUNCT_7:def_3;
then ((EmptyBag X) +* ( the Element of X,1)) . u = (EmptyBag X) . u by A6, FUNCT_4:11
.= 0 by PRE_POLY:52 ;
hence  contradiction by A5, PRE_POLY:def_7; ::_thesis: verum
end;
hence  u in { the Element of X} by TARSKI:def_1; ::_thesis: verum
end;
 the Element of X in dom ( the Element of X .--> 1) by A3, TARSKI:def_1;
then A7: ((EmptyBag X) +* ( the Element of X,1)) . the Element of X = ( the Element of X .--> 1) . the Element of X by A2, FUNCT_4:13
.= 1 by FUNCOP_1:72 ;
 for u being set st u in { the Element of X} holds
u in support ((EmptyBag X) +* ( the Element of X,1))
proof
let u be set ; ::_thesis: ( u in { the Element of X} implies u in support ((EmptyBag X) +* ( the Element of X,1)) )
assume  u in { the Element of X} ; ::_thesis: u in support ((EmptyBag X) +* ( the Element of X,1))
then  u = the Element of X by TARSKI:def_1;
hence  u in support ((EmptyBag X) +* ( the Element of X,1)) by A7, PRE_POLY:def_7; ::_thesis: verum
end;
then  support ((EmptyBag X) +* ( the Element of X,1)) = { the Element of X} by A4, TARSKI:1;
hence  (EmptyBag X) +* ( the Element of X,1) is univariate by Def2; ::_thesis: verum
end;
end;

registration
let X be non empty set ;
cluster Relation-like X -defined Function-like total V208() finite-support univariate  ->  non empty for set ;
coherence
 for b1 being bag of X st b1 is univariate holds
not b1 is empty
proof
let b be bag of X; ::_thesis: ( b is univariate implies not b is empty )
assume  b is univariate ; ::_thesis: not b is empty
then consider x being Element of X such that
A1: support b = {x} by Def2;
 x in support b by A1, TARSKI:def_1;
then  b . x <> 0 by PRE_POLY:def_7;
then  b . x <> (EmptyBag X) . x by PRE_POLY:52;
hence  not b is empty by POLYNOM2:def_1; ::_thesis: verum
end;
end;

begin

theorem :: POLYNOM7:3
for b being bag of {} holds b = EmptyBag {}
proof
set n = {} ;
let b be bag of {} ; ::_thesis: b = EmptyBag {}
A1: for b being bag of {} holds b = {}
proof
let b be bag of {} ; ::_thesis: b = {}
 b in Bags {} by PRE_POLY:def_12;
hence  b = {} by PRE_POLY:51, TARSKI:def_1; ::_thesis: verum
end;
then  EmptyBag {} = {} ;
hence  b = EmptyBag {} by A1; ::_thesis: verum
end;

Lm1:  for L being non empty doubleLoopStr
for p being Polynomial of {},L ex a being Element of L st p = {(EmptyBag {})} --> a
proof
set n = {} ;
let L be non empty doubleLoopStr ; ::_thesis: for p being Polynomial of {},L ex a being Element of L st p = {(EmptyBag {})} --> a
let p be Polynomial of {},L; ::_thesis: ex a being Element of L st p = {(EmptyBag {})} --> a
A1: for b being bag of {} holds b = {}
proof
let b be bag of {} ; ::_thesis: b = {}
 b in Bags {} by PRE_POLY:def_12;
hence  b = {} by PRE_POLY:51, TARSKI:def_1; ::_thesis: verum
end;
reconsider p = p as Function of (Bags {}),L ;
reconsider p = p as Function of {{}}, the carrier of L by PRE_POLY:51;
set a = p /. {};
A2: dom p = {{}} by FUNCT_2:def_1
.= {(EmptyBag {})} by A1 ;
A3: for u being set st u in p holds
u in [:{(EmptyBag {})},{(p /. {})}:]
proof
let u be set ; ::_thesis: ( u in p implies u in [:{(EmptyBag {})},{(p /. {})}:] )
assume A4: u in p ; ::_thesis: u in [:{(EmptyBag {})},{(p /. {})}:]
then consider p1, p2 being set  such that
A5: u = [p1,p2] by RELAT_1:def_1;
A6: p1 in dom p by A4, A5, XTUPLE_0:def_12;
then reconsider p1 = p1 as bag of {} by A2;
A7: p1 = {} by A1;
then p2 = p . {} by A4, A5, A6, FUNCT_1:def_2
.= p /. {} by A6, A7, PARTFUN1:def_6 ;
then  p2 in {(p /. {})} by TARSKI:def_1;
hence  u in [:{(EmptyBag {})},{(p /. {})}:] by A2, A5, A6, ZFMISC_1:def_2; ::_thesis: verum
end;
take  p /. {} ; ::_thesis: p = {(EmptyBag {})} --> (p /. {})
A8: EmptyBag {} = {} by A1;
 for u being set st u in [:{(EmptyBag {})},{(p /. {})}:] holds
u in p
proof
let u be set ; ::_thesis: ( u in [:{(EmptyBag {})},{(p /. {})}:] implies u in p )
assume  u in [:{(EmptyBag {})},{(p /. {})}:] ; ::_thesis: u in p
then consider u1, u2 being set  such that
A9: u1 in {(EmptyBag {})} and
A10: u2 in {(p /. {})} and
A11: u = [u1,u2] by ZFMISC_1:def_2;
A12: u1 = {} by A8, A9, TARSKI:def_1;
u2 = p /. {} by A10, TARSKI:def_1
.= p . {} by A2, A9, A12, PARTFUN1:def_6 ;
hence  u in p by A2, A9, A11, A12, FUNCT_1:1; ::_thesis: verum
end;
hence  p = {(EmptyBag {})} --> (p /. {}) by A3, TARSKI:1; ::_thesis: verum
end;

theorem :: POLYNOM7:4
for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of {},L
for x being Function of {},L holds eval (p,x) = p . (EmptyBag {})
proof
set n = {} ;
let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; ::_thesis: for p being Polynomial of {},L
for x being Function of {},L holds eval (p,x) = p . (EmptyBag {})
let p be Polynomial of {},L; ::_thesis: for x being Function of {},L holds eval (p,x) = p . (EmptyBag {})
let x be Function of {},L; ::_thesis: eval (p,x) = p . (EmptyBag {})
A1: for b being bag of {} holds b = {}
proof
let b be bag of {} ; ::_thesis: b = {}
 b in Bags {} by PRE_POLY:def_12;
hence  b = {} by PRE_POLY:51, TARSKI:def_1; ::_thesis: verum
end;
then A2: EmptyBag {} = {} ;
consider a being Element of L such that
A3: p = {(EmptyBag {})} --> a by Lm1;
A4: EmptyBag {} in {(EmptyBag {})} by TARSKI:def_1;
then A5: p . (EmptyBag {}) = a by A3, FUNCOP_1:7;
A6: dom p = {(EmptyBag {})} by A3, FUNCOP_1:13;
now__::_thesis:_(_(_a_=_0._L_&_eval_(p,x)_=_a_)_or_(_a_<>_0._L_&_eval_(p,x)_=_a_)_)
percases ( a = 0. L or a <> 0. L ) ;
caseA7: a = 0. L ; ::_thesis: eval (p,x) = a
 Support p = {}
proof
set u = the Element of Support p;
assume A8: Support p <> {} ; ::_thesis: contradiction
then  the Element of Support p in Support p ;
then reconsider u = the Element of Support p as Element of Bags {} ;
 p . u <> 0. L by A8, POLYNOM1:def_3;
hence  contradiction by A1, A2, A5, A7; ::_thesis: verum
end;
then reconsider Sp = Support p as empty Subset of (Bags {}) ;
consider y being FinSequence of the carrier of L such that
A9: len y = len (SgmX ((BagOrder {}),(Support p))) and
A10: eval (p,x) = Sum y and
 for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((p * (SgmX ((BagOrder {}),(Support p)))) /. i) * (eval ((((SgmX ((BagOrder {}),(Support p))) /. i) @),x)) by POLYNOM2:def_4;
 SgmX ((BagOrder {}),Sp) = {} by POLYNOM2:7, POLYNOM2:18;
then  y = <*> the carrier of L by A9;
hence  eval (p,x) = a by A7, A10, RLVECT_1:43; ::_thesis: verum
end;
caseA11: a <> 0. L ; ::_thesis: eval (p,x) = a
reconsider sp = Support p as finite Subset of (Bags {}) ;
set sg = SgmX ((BagOrder {}),sp);
A12: BagOrder {} linearly_orders sp by POLYNOM2:18;
A13: for u being set st u in Support p holds
u in {{}}
proof
let u be set ; ::_thesis: ( u in Support p implies u in {{}} )
assume  u in Support p ; ::_thesis: u in {{}}
then reconsider u = u as Element of Bags {} ;
 u = {} by A1;
hence  u in {{}} by TARSKI:def_1; ::_thesis: verum
end;
 for u being set st u in {{}} holds
u in Support p
proof
let u be set ; ::_thesis: ( u in {{}} implies u in Support p )
assume  u in {{}} ; ::_thesis: u in Support p
then  u = EmptyBag {} by A2, TARSKI:def_1;
hence  u in Support p by A5, A11, POLYNOM1:def_3; ::_thesis: verum
end;
then  Support p = {{}} by A13, TARSKI:1;
then A14: rng (SgmX ((BagOrder {}),sp)) = {{}} by A12, PRE_POLY:def_2;
then A15: {} in rng (SgmX ((BagOrder {}),sp)) by TARSKI:def_1;
then A16: 1 in dom (SgmX ((BagOrder {}),sp)) by FINSEQ_3:31;
then  (SgmX ((BagOrder {}),sp)) . 1 in dom p by A2, A6, A14, FUNCT_1:3;
then  1 in dom (p * (SgmX ((BagOrder {}),sp))) by A16, FUNCT_1:11;
then A17: (p * (SgmX ((BagOrder {}),sp))) /. 1 = (p * (SgmX ((BagOrder {}),sp))) . 1 by PARTFUN1:def_6
.= p . ((SgmX ((BagOrder {}),sp)) . 1) by A16, FUNCT_1:13
.= a by A2, A3, A14, A16, FUNCOP_1:7, FUNCT_1:3 ;
A18: for u being set st u in dom (SgmX ((BagOrder {}),sp)) holds
u in {1}
proof
let u be set ; ::_thesis: ( u in dom (SgmX ((BagOrder {}),sp)) implies u in {1} )
assume A19: u in dom (SgmX ((BagOrder {}),sp)) ; ::_thesis: u in {1}
assume A20: not u in {1} ; ::_thesis: contradiction
reconsider u = u as Element of NAT by A19;
 (SgmX ((BagOrder {}),sp)) /. u = (SgmX ((BagOrder {}),sp)) . u by A19, PARTFUN1:def_6;
then A21: (SgmX ((BagOrder {}),sp)) /. u in rng (SgmX ((BagOrder {}),sp)) by A19, FUNCT_1:3;
A22: u <> 1 by A20, TARSKI:def_1;
A23: 1 < u
proof
consider k being Nat such that
A24: dom (SgmX ((BagOrder {}),sp)) = Seg k by FINSEQ_1:def_2;
 Seg k =  {  m where m is Element of NAT : ( 1 <= m & m <= k )  }  by FINSEQ_1:def_1;
then  ex m9 being Element of NAT st
( m9 = u & 1 <= m9 & m9 <= k ) by A19, A24;
hence  1 < u by A22, XXREAL_0:1; ::_thesis: verum
end;
 (SgmX ((BagOrder {}),sp)) /. 1 = (SgmX ((BagOrder {}),sp)) . 1 by A15, A19, FINSEQ_3:31, PARTFUN1:def_6;
then  (SgmX ((BagOrder {}),sp)) /. 1 in rng (SgmX ((BagOrder {}),sp)) by A16, FUNCT_1:3;
then (SgmX ((BagOrder {}),sp)) /. 1 = {} by A14, TARSKI:def_1
.= (SgmX ((BagOrder {}),sp)) /. u by A14, A21, TARSKI:def_1 ;
hence  contradiction by A12, A16, A19, A23, PRE_POLY:def_2; ::_thesis: verum
end;
 for u being set st u in {1} holds
u in dom (SgmX ((BagOrder {}),sp)) by A16, TARSKI:def_1;
then  dom (SgmX ((BagOrder {}),sp)) = Seg 1 by A18, FINSEQ_1:2, TARSKI:1;
then A25: len (SgmX ((BagOrder {}),sp)) = 1 by FINSEQ_1:def_3;
consider y being FinSequence of the carrier of L such that
A26: len y = len (SgmX ((BagOrder {}),sp)) and
A27: Sum y = eval (p,x) and
A28: for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((p * (SgmX ((BagOrder {}),sp))) /. i) * (eval ((((SgmX ((BagOrder {}),sp)) /. i) @),x)) by POLYNOM2:def_4;
dom y = Seg (len y) by FINSEQ_1:def_3
.= dom (SgmX ((BagOrder {}),sp)) by A26, FINSEQ_1:def_3 ;
then y . 1 = y /. 1 by A15, FINSEQ_3:31, PARTFUN1:def_6
.= ((p * (SgmX ((BagOrder {}),sp))) /. 1) * (eval ((((SgmX ((BagOrder {}),sp)) /. 1) @),x)) by A25, A26, A28
.= ((p * (SgmX ((BagOrder {}),sp))) /. 1) * (eval ((EmptyBag {}),x)) by A1, A2
.= ((p * (SgmX ((BagOrder {}),sp))) /. 1) * (1. L) by POLYNOM2:14
.= a by A17, VECTSP_1:def_4 ;
then  y = <*a*> by A25, A26, FINSEQ_1:40;
hence  eval (p,x) = a by A27, RLVECT_1:44; ::_thesis: verum
end;
end;
end;
hence  eval (p,x) = p . (EmptyBag {}) by A3, A4, FUNCOP_1:7; ::_thesis: verum
end;

theorem :: POLYNOM7:5
for L being non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr holds Polynom-Ring ({},L) is_ringisomorph_to L
proof
set n = {} ;
let L be non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: Polynom-Ring ({},L) is_ringisomorph_to L
set PL = Polynom-Ring ({},L);
defpred S1[ set , set ] means  ex p being Polynomial of {},L st
( p = $1 & p . {} = $2 );
A1: dom (0_ ({},L)) = Bags {} by FUNCT_2:def_1;
 dom ((EmptyBag {}) .--> (1_ L)) = {(EmptyBag {})} by FUNCOP_1:13;
then A2: EmptyBag {} in dom ((EmptyBag {}) .--> (1_ L)) by TARSKI:def_1;
A3: for b being bag of {} holds b = {}
proof
let b be bag of {} ; ::_thesis: b = {}
 b in Bags {} by PRE_POLY:def_12;
hence  b = {} by PRE_POLY:51, TARSKI:def_1; ::_thesis: verum
end;
then A4: EmptyBag {} = {} ;
then reconsider i = {} as bag of {} ;
A5: for x being Element of (Polynom-Ring ({},L)) ex y being Element of L st S1[x,y]
proof
let x be Element of (Polynom-Ring ({},L)); ::_thesis: ex y being Element of L st S1[x,y]
reconsider p = x as Polynomial of {},L by POLYNOM1:def_10;
take  p . {} ; ::_thesis: ( p . {} is Element of L & S1[x,p . {}] )
 dom p = Bags {} by FUNCT_2:def_1;
then A6: p . {} in rng p by A4, FUNCT_1:3;
 rng p c= the carrier of L by RELAT_1:def_19;
hence  ( p . {} is Element of L & S1[x,p . {}] ) by A6; ::_thesis: verum
end;
consider f being Function of the carrier of (Polynom-Ring ({},L)), the carrier of L such that
A7: for x being Element of (Polynom-Ring ({},L)) holds S1[x,f . x] from FUNCT_2:sch_3(A5);
A8: dom f = the carrier of (Polynom-Ring ({},L)) by FUNCT_2:def_1;
reconsider f = f as Function of (Polynom-Ring ({},L)),L ;
consider p being Polynomial of {},L such that
A9: p = 1_ (Polynom-Ring ({},L)) and
A10: p . {} = f . (1. (Polynom-Ring ({},L))) by A7;
A11: p = 1_ ({},L) by A9, POLYNOM1:31
.= (0_ ({},L)) +* ((EmptyBag {}),(1_ L)) by POLYNOM1:def_8 ;
 for x, y being Element of (Polynom-Ring ({},L)) holds f . (x * y) = (f . x) * (f . y)
proof
let x, y be Element of (Polynom-Ring ({},L)); ::_thesis: f . (x * y) = (f . x) * (f . y)
consider p being Polynomial of {},L such that
A12: ( p = x & p . {} = f . x ) by A7;
consider q being Polynomial of {},L such that
A13: ( q = y & q . {} = f . y ) by A7;
A14: (p *' q) . {} = (p . i) * (q . i)
proof
A15: decomp (EmptyBag {}) = <*<*(EmptyBag {}),(EmptyBag {})*>*> by PRE_POLY:73;
then A16: len (decomp (EmptyBag {})) = 1 by FINSEQ_1:39;
set z = (p . i) * (q . i);
consider s being FinSequence of the carrier of L such that
A17: (p *' q) . (EmptyBag {}) = Sum s and
A18: len s = len (decomp (EmptyBag {})) and
A19: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of {} st
( (decomp (EmptyBag {})) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) by POLYNOM1:def_9;
 len s = 1 by A15, A18, FINSEQ_1:39;
then  Seg 1 = dom s by FINSEQ_1:def_3;
then A20: 1 in dom s by FINSEQ_1:2, TARSKI:def_1;
then consider b1, b2 being bag of {}  such that
 (decomp (EmptyBag {})) /. 1 = <*b1,b2*> and
A21: s /. 1 = (p . b1) * (q . b2) by A19;
s . 1 = (p . b1) * (q . b2) by A20, A21, PARTFUN1:def_6
.= (p . i) * (q . b2) by A3
.= (p . i) * (q . i) by A3 ;
then  s = <*((p . i) * (q . i))*> by A16, A18, FINSEQ_1:40;
then  Sum s = (p . i) * (q . i) by RLVECT_1:44;
hence  (p *' q) . {} = (p . i) * (q . i) by A3, A17; ::_thesis: verum
end;
 ex pq being Polynomial of {},L st
( pq = x * y & pq . {} = f . (x * y) ) by A7;
hence  f . (x * y) = (f . x) * (f . y) by A12, A13, A14, POLYNOM1:def_10; ::_thesis: verum
end;
then A22: f is multiplicative by GROUP_6:def_6;
 for x, y being Element of (Polynom-Ring ({},L)) holds f . (x + y) = (f . x) + (f . y)
proof
let x, y be Element of (Polynom-Ring ({},L)); ::_thesis: f . (x + y) = (f . x) + (f . y)
consider p being Polynomial of {},L such that
A23: p = x and
A24: p . {} = f . x by A7;
consider q being Polynomial of {},L such that
A25: q = y and
A26: q . {} = f . y by A7;
consider a being Element of L such that
A27: p = {(EmptyBag {})} --> a by Lm1;
A28: ex pq being Polynomial of {},L st
( pq = x + y & pq . {} = f . (x + y) ) by A7;
consider b being Element of L such that
A29: q = {(EmptyBag {})} --> b by Lm1;
A30: EmptyBag {} in {(EmptyBag {})} by TARSKI:def_1;
then A31: p . {} = a by A4, A27, FUNCOP_1:7;
A32: (p + q) . {} = (p . i) + (q . i) by POLYNOM1:15
.= a + b by A4, A30, A31, A29, FUNCOP_1:7 ;
 q . {} = b by A4, A30, A29, FUNCOP_1:7;
then  (f . x) + (f . y) = a + b by A4, A24, A26, A27, A30, FUNCOP_1:7;
hence  f . (x + y) = (f . x) + (f . y) by A23, A25, A28, A32, POLYNOM1:def_10; ::_thesis: verum
end;
then A33: f is additive by VECTSP_1:def_20;
p . i = p . (EmptyBag {}) by A3
.= ((0_ ({},L)) +* ((EmptyBag {}) .--> (1_ L))) . (EmptyBag {}) by A11, A1, FUNCT_7:def_3
.= ((EmptyBag {}) .--> (1_ L)) . (EmptyBag {}) by A2, FUNCT_4:13
.= 1_ L by FUNCOP_1:72 ;
then  f is unity-preserving by A9, A10, GROUP_1:def_13;
then A34: f is RingHomomorphism by A33, A22, QUOFIELD:def_18;
A35: for u being set st u in the carrier of L holds
u in rng f
proof
let u be set ; ::_thesis: ( u in the carrier of L implies u in rng f )
assume  u in the carrier of L ; ::_thesis: u in rng f
then reconsider u = u as Element of L ;
set p = (EmptyBag {}) .--> u;
reconsider p = (EmptyBag {}) .--> u as Function ;
 dom p = {(EmptyBag {})} by FUNCOP_1:13;
then  ( rng p = {u} & dom p = Bags {} ) by FUNCOP_1:8, PRE_POLY:51, TARSKI:def_1;
then reconsider p = p as Function of (Bags {}), the carrier of L by FUNCT_2:2;
reconsider p = p as Function of (Bags {}),L ;
reconsider p = p as Series of {},L ;
now__::_thesis:_(_(_u_=_0._L_&_Support_p_is_finite_)_or_(_u_<>_0._L_&_Support_p_is_finite_)_)
percases ( u = 0. L or u <> 0. L ) ;
caseA36: u = 0. L ; ::_thesis: Support p is finite
 Support p = {}
proof
set v = the Element of Support p;
assume  Support p <> {} ; ::_thesis: contradiction
then A37: the Element of Support p in Support p ;
then  the Element of Support p is bag of {} ;
then p . the Element of Support p = p . (EmptyBag {}) by A3, A4
.= u by FUNCOP_1:72 ;
hence  contradiction by A36, A37, POLYNOM1:def_3; ::_thesis: verum
end;
hence  Support p is finite ; ::_thesis: verum
end;
caseA38: u <> 0. L ; ::_thesis: Support p is finite
A39: for v being set st v in {(EmptyBag {})} holds
v in Support p
proof
let v be set ; ::_thesis: ( v in {(EmptyBag {})} implies v in Support p )
assume A40: v in {(EmptyBag {})} ; ::_thesis: v in Support p
then reconsider v = v as Element of Bags {} ;
p . v = p . (EmptyBag {}) by A40, TARSKI:def_1
.= u by FUNCOP_1:72 ;
hence  v in Support p by A38, POLYNOM1:def_3; ::_thesis: verum
end;
 for v being set st v in Support p holds
v in {(EmptyBag {})}
proof
let v be set ; ::_thesis: ( v in Support p implies v in {(EmptyBag {})} )
assume  v in Support p ; ::_thesis: v in {(EmptyBag {})}
then reconsider v = v as bag of {} ;
 v = EmptyBag {} by A3, A4;
hence  v in {(EmptyBag {})} by TARSKI:def_1; ::_thesis: verum
end;
hence  Support p is finite by A39, TARSKI:1; ::_thesis: verum
end;
end;
end;
then reconsider p = p as Polynomial of {},L by POLYNOM1:def_4;
reconsider p9 = p as Element of (Polynom-Ring ({},L)) by POLYNOM1:def_10;
consider q being Polynomial of {},L such that
A41: q = p9 and
A42: q . {} = f . p9 by A7;
q . {} = p . (EmptyBag {}) by A3, A41
.= u by FUNCOP_1:72 ;
hence  u in rng f by A8, A42, FUNCT_1:3; ::_thesis: verum
end;
 rng f c= the carrier of L by RELAT_1:def_19;
then  for u being set st u in rng f holds
u in the carrier of L ;
then  rng f = the carrier of L by A35, TARSKI:1;
then A43: f is RingEpimorphism by A34, QUOFIELD:def_19;
 for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A44: ( x1 in dom f & x2 in dom f ) and
A45: f . x1 = f . x2 ; ::_thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Element of (Polynom-Ring ({},L)) by A44;
consider p being Polynomial of {},L such that
A46: ( p = x1 & p . {} = f . x1 ) by A7;
consider q being Polynomial of {},L such that
A47: ( q = x2 & q . {} = f . x2 ) by A7;
consider a2 being Element of L such that
A48: q = {(EmptyBag {})} --> a2 by Lm1;
A49: EmptyBag {} in {(EmptyBag {})} by TARSKI:def_1;
then A50: q . (EmptyBag {}) = a2 by A48, FUNCOP_1:7;
A51: p . {} = p . (EmptyBag {}) by A3;
consider a1 being Element of L such that
A52: p = {(EmptyBag {})} --> a1 by Lm1;
 p . (EmptyBag {}) = a1 by A52, A49, FUNCOP_1:7;
hence  x1 = x2 by A3, A45, A46, A47, A52, A48, A50, A51; ::_thesis: verum
end;
then  f is one-to-one by FUNCT_1:def_4;
then  f is RingMonomorphism by A34, QUOFIELD:def_20;
then  f is RingIsomorphism by A43, QUOFIELD:def_21;
hence  Polynom-Ring ({},L) is_ringisomorph_to L by QUOFIELD:def_23; ::_thesis: verum
end;

begin

definition
let X be set ;
let L be non empty ZeroStr ;
let p be Series of X,L;
attrp is monomial-like  means :Def3: :: POLYNOM7:def 3
 ex b being bag of X st
for b9 being bag of X st b9 <> b holds
p . b9 = 0. L;
end;

:: deftheorem Def3 defines monomial-like POLYNOM7:def_3_:_
 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 );

registration
let X be set ;
let L be non empty ZeroStr ;
cluster Relation-like Bags X -defined the carrier of L -valued Function-like V18( Bags X, the carrier of L) monomial-like for Element of bool [:(Bags X), the carrier of L:];
existence
 ex b1 being Series of X,L st b1 is monomial-like
proof
set p = 0_ (X,L);
take  0_ (X,L) ; ::_thesis: 0_ (X,L) is monomial-like
 for b9 being bag of X st b9 <> EmptyBag X holds
(0_ (X,L)) . b9 = 0. L by POLYNOM1:22;
hence  0_ (X,L) is monomial-like by Def3; ::_thesis: verum
end;
end;

definition
let X be set ;
let L be non empty ZeroStr ;
mode Monomial of X,L is monomial-like Series of X,L;
end;

registration
let X be set ;
let L be non empty ZeroStr ;
cluster Function-like V18( Bags X, the carrier of L) monomial-like  ->  finite-Support for Element of bool [:(Bags X), the carrier of L:];
coherence
 for b1 being Series of X,L st b1 is monomial-like holds
b1 is finite-Support
proof
let s be Series of X,L; ::_thesis: ( s is monomial-like implies s is finite-Support )
assume  s is monomial-like ; ::_thesis: s is finite-Support
then consider b being bag of X such that
A1: for b9 being bag of X st b9 <> b holds
s . b9 = 0. L by Def3;
percases ( s . b = 0. L or s . b <> 0. L ) ;
supposeA2: s . b = 0. L ; ::_thesis: s is finite-Support
now__::_thesis:_not_Support_s_<>_{}
assume  Support s <> {} ; ::_thesis: contradiction
then reconsider sp = Support s as non empty Subset of (Bags X) ;
set c = the Element of sp;
 s . the Element of sp <> 0. L by POLYNOM1:def_3;
hence  contradiction by A1, A2; ::_thesis: verum
end;
hence  s is finite-Support by POLYNOM1:def_4; ::_thesis: verum
end;
supposeA3: s . b <> 0. L ; ::_thesis: s is finite-Support
A4: now__::_thesis:_for_u_being_set_st_u_in_Support_s_holds_
u_in_{b}
let u be set ; ::_thesis: ( u in Support s implies u in {b} )
assume A5: u in Support s ; ::_thesis: u in {b}
then reconsider u9 = u as Element of Bags X ;
 s . u9 <> 0. L by A5, POLYNOM1:def_3;
then  u9 = b by A1;
hence  u in {b} by TARSKI:def_1; ::_thesis: verum
end;
now__::_thesis:_for_u_being_set_st_u_in_{b}_holds_
u_in_Support_s
let u be set ; ::_thesis: ( u in {b} implies u in Support s )
assume  u in {b} ; ::_thesis: u in Support s
then A6: u = b by TARSKI:def_1;
then reconsider u9 = u as Element of Bags X by PRE_POLY:def_12;
 u9 in Support s by A3, A6, POLYNOM1:def_3;
hence  u in Support s ; ::_thesis: verum
end;
then  Support s = {b} by A4, TARSKI:1;
hence  s is finite-Support by POLYNOM1:def_4; ::_thesis: verum
end;
end;
end;
end;

theorem Th6: :: POLYNOM7:6
for X being set
for L being non empty ZeroStr
for p being Series of X,L holds
( p is Monomial of X,L iff ( Support p = {} or ex b being bag of X st Support p = {b} ) )
proof
let n be set ; ::_thesis: for L being non empty ZeroStr
for p being Series of n,L holds
( p is Monomial of n,L iff ( Support p = {} or ex b being bag of n st Support p = {b} ) )
let L be non empty ZeroStr ; ::_thesis: for p being Series of n,L holds
( p is Monomial of n,L iff ( Support p = {} or ex b being bag of n st Support p = {b} ) )
let p be Series of n,L; ::_thesis: ( p is Monomial of n,L iff ( Support p = {} or ex b being bag of n st Support p = {b} ) )
A1: now__::_thesis:_(_ex_b_being_bag_of_n_st_Support_p_=_{b}_implies_p_is_Monomial_of_n,L_)
assume  ex b being bag of n st Support p = {b} ; ::_thesis: p is Monomial of n,L
then consider b being bag of n such that
A2: Support p = {b} ;
 for b9 being bag of n st b9 <> b holds
p . b9 = 0. L
proof
let b9 be bag of n; ::_thesis: ( b9 <> b implies p . b9 = 0. L )
assume A3: b9 <> b ; ::_thesis: p . b9 = 0. L
assume A4: p . b9 <> 0. L ; ::_thesis: contradiction
reconsider b9 = b9 as Element of Bags n by PRE_POLY:def_12;
 b9 in Support p by A4, POLYNOM1:def_3;
hence  contradiction by A2, A3, TARSKI:def_1; ::_thesis: verum
end;
hence  p is Monomial of n,L by Def3; ::_thesis: verum
end;
A5: now__::_thesis:_(_not_p_is_Monomial_of_n,L_or_Support_p_=_{}_or_ex_b_being_bag_of_n_st_Support_p_=_{b}_)
assume  p is Monomial of n,L ; ::_thesis: ( Support p = {} or ex b being bag of n st Support p = {b} )
then consider b being bag of n such that
A6: for b9 being bag of n st b9 <> b holds
p . b9 = 0. L by Def3;
now__::_thesis:_(_(_p_._b_<>_0._L_&_ex_b_being_bag_of_n_st_Support_p_=_{b}_)_or_(_p_._b_=_0._L_&_Support_p_=_{}_)_)
percases ( p . b <> 0. L or p . b = 0. L ) ;
caseA7: p . b <> 0. L ; ::_thesis: ex b being bag of n st Support p = {b}
A8: for u being set st u in {b} holds
u in Support p
proof
let u be set ; ::_thesis: ( u in {b} implies u in Support p )
assume A9: u in {b} ; ::_thesis: u in Support p
then  u = b by TARSKI:def_1;
then reconsider u9 = u as Element of Bags n by PRE_POLY:def_12;
 p . u9 <> 0. L by A7, A9, TARSKI:def_1;
hence  u in Support p by POLYNOM1:def_3; ::_thesis: verum
end;
 for u being set st u in Support p holds
u in {b}
proof
let u be set ; ::_thesis: ( u in Support p implies u in {b} )
assume A10: u in Support p ; ::_thesis: u in {b}
then reconsider u9 = u as bag of n ;
 p . u <> 0. L by A10, POLYNOM1:def_3;
then  u9 = b by A6;
hence  u in {b} by TARSKI:def_1; ::_thesis: verum
end;
then  Support p = {b} by A8, TARSKI:1;
hence  ex b being bag of n st Support p = {b} ; ::_thesis: verum
end;
caseA11: p . b = 0. L ; ::_thesis: Support p = {}
thus  Support p = {} ::_thesis: verum
proof
assume  Support p <> {} ; ::_thesis: contradiction
then reconsider sp = Support p as non empty Subset of (Bags n) ;
set c = the Element of sp;
 p . the Element of sp <> 0. L by POLYNOM1:def_3;
hence  contradiction by A6, A11; ::_thesis: verum
end;
end;
end;
end;
hence  ( Support p = {} or ex b being bag of n st Support p = {b} ) ; ::_thesis: verum
end;
now__::_thesis:_(_Support_p_=_{}_implies_p_is_Monomial_of_n,L_)
set b = the bag of n;
assume A12: Support p = {} ; ::_thesis: p is Monomial of n,L
 for b9 being bag of n st b9 <> the bag of n holds
p . b9 = 0. L
proof
let b9 be bag of n; ::_thesis: ( b9 <> the bag of n implies p . b9 = 0. L )
assume  b9 <> the bag of n ; ::_thesis: p . b9 = 0. L
reconsider c = b9 as Element of Bags n by PRE_POLY:def_12;
assume  p . b9 <> 0. L ; ::_thesis: contradiction
then  c in Support p by POLYNOM1:def_3;
hence  contradiction by A12; ::_thesis: verum
end;
hence  p is Monomial of n,L by Def3; ::_thesis: verum
end;
hence  ( p is Monomial of n,L iff ( Support p = {} or ex b being bag of n st Support p = {b} ) ) by A1, A5; ::_thesis: verum
end;

definition
let X be set ;
let L be non empty ZeroStr ;
let a be Element of L;
let b be bag of X;
func Monom (a,b) ->  Monomial of X,L equals :: POLYNOM7:def 4
(0_ (X,L)) +* (b,a);
coherence
 (0_ (X,L)) +* (b,a) is Monomial of X,L
proof
 dom (b .--> a) = {b} by FUNCOP_1:13;
then A1: b in dom (b .--> a) by TARSKI:def_1;
set m = (0_ (X,L)) +* (b,a);
reconsider m = (0_ (X,L)) +* (b,a) as Function of (Bags X), the carrier of L ;
reconsider m = m as Function of (Bags X),L ;
reconsider m = m as Series of X,L ;
A2: b in Bags X by PRE_POLY:def_12;
A3: dom (0_ (X,L)) = dom ((Bags X) --> (0. L)) by POLYNOM1:def_7
.= Bags X by FUNCOP_1:13 ;
then A4: m = (0_ (X,L)) +* (b .--> a) by A2, FUNCT_7:def_3;
A5: m . b = ((0_ (X,L)) +* (b .--> a)) . b by A3, A2, FUNCT_7:def_3
.= (b .--> a) . b by A1, FUNCT_4:13
.= a by FUNCOP_1:72 ;
now__::_thesis:_(_(_a_<>_0._L_&_(0__(X,L))_+*_(b,a)_is_Monomial_of_X,L_)_or_(_a_=_0._L_&_(0__(X,L))_+*_(b,a)_is_Monomial_of_X,L_)_)
percases ( a <> 0. L or a = 0. L ) ;
caseA6: a <> 0. L ; ::_thesis: (0_ (X,L)) +* (b,a) is Monomial of X,L
A7: for u being set st u in Support m holds
u in {b}
proof
let u be set ; ::_thesis: ( u in Support m implies u in {b} )
assume A8: u in Support m ; ::_thesis: u in {b}
assume  not u in {b} ; ::_thesis: contradiction
then A9: not u in dom (b .--> a) ;
reconsider u = u as bag of X by A8;
m . u = (0_ (X,L)) . u by A4, A9, FUNCT_4:11
.= 0. L by POLYNOM1:22 ;
hence  contradiction by A8, POLYNOM1:def_3; ::_thesis: verum
end;
 b in Support m by A2, A5, A6, POLYNOM1:def_3;
then  for u being set st u in {b} holds
u in Support m by TARSKI:def_1;
then  Support m = {b} by A7, TARSKI:1;
hence  (0_ (X,L)) +* (b,a) is Monomial of X,L by Th6; ::_thesis: verum
end;
caseA10: a = 0. L ; ::_thesis: (0_ (X,L)) +* (b,a) is Monomial of X,L
now__::_thesis:_not_Support_m_<>_{}
assume  Support m <> {} ; ::_thesis: contradiction
then reconsider sm = Support m as non empty Subset of (Bags X) ;
set c = the Element of sm;
 m . the Element of sm <> 0. L by POLYNOM1:def_3;
then  not the Element of sm in {b} by A5, A10, TARSKI:def_1;
then A11: not the Element of sm in dom (b .--> a) ;
reconsider c = the Element of sm as bag of X ;
m . c = (0_ (X,L)) . c by A4, A11, FUNCT_4:11
.= 0. L by POLYNOM1:22 ;
hence  contradiction by POLYNOM1:def_3; ::_thesis: verum
end;
hence  (0_ (X,L)) +* (b,a) is Monomial of X,L by Th6; ::_thesis: verum
end;
end;
end;
hence  (0_ (X,L)) +* (b,a) is Monomial of X,L ; ::_thesis: verum
end;
end;

:: deftheorem  defines Monom POLYNOM7:def_4_:_
 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);

definition
let X be set ;
let L be non empty ZeroStr ;
let m be Monomial of X,L;
func term m ->  bag of X means :Def5: :: POLYNOM7:def 5
( m . it <> 0. L or ( Support m = {} & it = EmptyBag X ) );
existence
 ex b1 being bag of X st
( m . b1 <> 0. L or ( Support m = {} & b1 = EmptyBag X ) )
proof
consider b being bag of X such that
A1: for b9 being bag of X st b9 <> b holds
m . b9 = 0. L by Def3;
now__::_thesis:_(_(_m_._b_<>_0._L_&_ex_b1_being_bag_of_X_st_
(_m_._b1_<>_0._L_or_(_Support_m_=_{}_&_b1_=_EmptyBag_X_)_)_)_or_(_m_._b_=_0._L_&_ex_b1_being_bag_of_X_st_
(_m_._b1_<>_0._L_or_(_Support_m_=_{}_&_b1_=_EmptyBag_X_)_)_)_)
percases ( m . b <> 0. L or m . b = 0. L ) ;
case m . b <> 0. L ; ::_thesis: ex b1 being bag of X st
( m . b1 <> 0. L or ( Support m = {} & b1 = EmptyBag X ) )
hence  ex b1 being bag of X st
( m . b1 <> 0. L or ( Support m = {} & b1 = EmptyBag X ) ) ; ::_thesis: verum
end;
caseA2: m . b = 0. L ; ::_thesis: ex b1 being bag of X st
( m . b1 <> 0. L or ( Support m = {} & b1 = EmptyBag X ) )
 Support m = {}
proof
assume  Support m <> {} ; ::_thesis: contradiction
then reconsider sm = Support m as non empty Subset of (Bags X) ;
set c = the Element of sm;
 m . the Element of sm <> 0. L by POLYNOM1:def_3;
hence  contradiction by A1, A2; ::_thesis: verum
end;
hence  ex b1 being bag of X st
( m . b1 <> 0. L or ( Support m = {} & b1 = EmptyBag X ) ) ; ::_thesis: verum
end;
end;
end;
hence  ex b1 being bag of X st
( m . b1 <> 0. L or ( Support m = {} & b1 = EmptyBag X ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being bag of X st ( m . b1 <> 0. L or ( Support m = {} & b1 = EmptyBag X ) ) & ( m . b2 <> 0. L or ( Support m = {} & b2 = EmptyBag X ) ) holds
b1 = b2
proof
let b1, b2 be bag of X; ::_thesis: ( ( m . b1 <> 0. L or ( Support m = {} & b1 = EmptyBag X ) ) & ( m . b2 <> 0. L or ( Support m = {} & b2 = EmptyBag X ) ) implies b1 = b2 )
assume A3: ( m . b1 <> 0. L or ( Support m = {} & b1 = EmptyBag X ) ) ; ::_thesis: ( ( not m . b2 <> 0. L & not ( Support m = {} & b2 = EmptyBag X ) ) or b1 = b2 )
consider b being bag of X such that
A4: for b9 being bag of X st b9 <> b holds
m . b9 = 0. L by Def3;
assume A5: ( m . b2 <> 0. L or ( Support m = {} & b2 = EmptyBag X ) ) ; ::_thesis: b1 = b2
now__::_thesis:_(_(_m_._b1_<>_0._L_&_b1_=_b2_)_or_(_m_._b1_=_0._L_&_b1_=_b2_)_)
percases ( m . b1 <> 0. L or m . b1 = 0. L ) ;
caseA6: m . b1 <> 0. L ; ::_thesis: b1 = b2
reconsider b19 = b1 as Element of Bags X by PRE_POLY:def_12;
A7: b19 in Support m by A6, POLYNOM1:def_3;
thus b1 = b by A4, A6
.= b2 by A5, A4, A7 ; ::_thesis: verum
end;
caseA8: m . b1 = 0. L ; ::_thesis: b1 = b2
now__::_thesis:_(_(_m_._b2_<>_0._L_&_b1_=_b2_)_or_(_Support_m_=_{}_&_b2_=_EmptyBag_X_&_b1_=_b2_)_)
percases ( m . b2 <> 0. L or ( Support m = {} & b2 = EmptyBag X ) ) by A5;
caseA9: m . b2 <> 0. L ; ::_thesis: b1 = b2
reconsider b29 = b2 as Element of Bags X by PRE_POLY:def_12;
 b29 in Support m by A9, POLYNOM1:def_3;
hence  b1 = b2 by A3, A8; ::_thesis: verum
end;
case ( Support m = {} & b2 = EmptyBag X ) ; ::_thesis: b1 = b2
hence  b1 = b2 by A3, A8; ::_thesis: verum
end;
end;
end;
hence  b1 = b2 ; ::_thesis: verum
end;
end;
end;
hence  b1 = b2 ; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines term POLYNOM7:def_5_:_
 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 ) ) );

definition
let X be set ;
let L be non empty ZeroStr ;
let m be Monomial of X,L;
func coefficient m ->  Element of L equals :: POLYNOM7:def 6
m . (term m);
coherence
 m . (term m) is Element of L ;
end;

:: deftheorem  defines coefficient POLYNOM7:def_6_:_
 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: :: POLYNOM7:7
for X being set
for L being non empty ZeroStr
for m being Monomial of X,L holds
( Support m = {} or Support m = {(term m)} )
proof
let X be set ; ::_thesis: for L being non empty ZeroStr
for m being Monomial of X,L holds
( Support m = {} or Support m = {(term m)} )
let L be non empty ZeroStr ; ::_thesis: for m being Monomial of X,L holds
( Support m = {} or Support m = {(term m)} )
let m be Monomial of X,L; ::_thesis: ( Support m = {} or Support m = {(term m)} )
A1: term m is Element of Bags X by PRE_POLY:def_12;
assume A2: Support m <> {} ; ::_thesis: Support m = {(term m)}
then  m . (term m) <> 0. L by Def5;
then A3: term m in Support m by A1, POLYNOM1:def_3;
 ex b being bag of X st Support m = {b} by A2, Th6;
hence  Support m = {(term m)} by A3, TARSKI:def_1; ::_thesis: verum
end;

theorem Th8: :: POLYNOM7:8
for X being set
for L being non empty ZeroStr
for b being bag of X holds
( coefficient (Monom ((0. L),b)) = 0. L & term (Monom ((0. L),b)) = EmptyBag X )
proof
let n be set ; ::_thesis: for L being non empty ZeroStr
for b being bag of n holds
( coefficient (Monom ((0. L),b)) = 0. L & term (Monom ((0. L),b)) = EmptyBag n )
let L be non empty ZeroStr ; ::_thesis: for b being bag of n holds
( coefficient (Monom ((0. L),b)) = 0. L & term (Monom ((0. L),b)) = EmptyBag n )
let b be bag of n; ::_thesis: ( coefficient (Monom ((0. L),b)) = 0. L & term (Monom ((0. L),b)) = EmptyBag n )
set m = (0_ (n,L)) +* (b,(0. L));
reconsider m = (0_ (n,L)) +* (b,(0. L)) as Function of (Bags n), the carrier of L ;
reconsider m = m as Function of (Bags n),L ;
reconsider m = m as Series of n,L ;
A1: b in Bags n by PRE_POLY:def_12;
A2: dom (0_ (n,L)) = dom ((Bags n) --> (0. L)) by POLYNOM1:def_7
.= Bags n by FUNCOP_1:13 ;
then A3: m = (0_ (n,L)) +* (b .--> (0. L)) by A1, FUNCT_7:def_3;
 dom (b .--> (0. L)) = {b} by FUNCOP_1:13;
then A4: b in dom (b .--> (0. L)) by TARSKI:def_1;
A5: m . b = ((0_ (n,L)) +* (b .--> (0. L))) . b by A2, A1, FUNCT_7:def_3
.= (b .--> (0. L)) . b by A4, FUNCT_4:13
.= 0. L by FUNCOP_1:72 ;
A6: now__::_thesis:_for_b9_being_bag_of_n_holds_m_._b9_=_0._L
let b9 be bag of n; ::_thesis: m . b9 = 0. L
now__::_thesis:_(_(_b9_=_b_&_m_._b9_=_0._L_)_or_(_b9_<>_b_&_m_._b9_=_0._L_)_)
percases ( b9 = b or b9 <> b ) ;
case b9 = b ; ::_thesis: m . b9 = 0. L
hence  m . b9 = 0. L by A5; ::_thesis: verum
end;
case b9 <> b ; ::_thesis: m . b9 = 0. L
then  not b9 in dom (b .--> (0. L)) by TARSKI:def_1;
hence m . b9 = (0_ (n,L)) . b9 by A3, FUNCT_4:11
.= 0. L by POLYNOM1:22 ;
::_thesis: verum
end;
end;
end;
hence  m . b9 = 0. L ; ::_thesis: verum
end;
hence  coefficient (Monom ((0. L),b)) = 0. L ; ::_thesis: term (Monom ((0. L),b)) = EmptyBag n
 (Monom ((0. L),b)) . (term (Monom ((0. L),b))) = 0. L by A6;
hence  term (Monom ((0. L),b)) = EmptyBag n by Def5; ::_thesis: verum
end;

theorem Th9: :: POLYNOM7:9
for X being set
for L being non empty ZeroStr
for a being Element of L
for b being bag of X holds coefficient (Monom (a,b)) = a
proof
let n be set ; ::_thesis: for L being non empty ZeroStr
for a being Element of L
for b being bag of n holds coefficient (Monom (a,b)) = a
let L be non empty ZeroStr ; ::_thesis: for a being Element of L
for b being bag of n holds coefficient (Monom (a,b)) = a
let a be Element of L; ::_thesis: for b being bag of n holds coefficient (Monom (a,b)) = a
let b be bag of n; ::_thesis: coefficient (Monom (a,b)) = a
set m = (0_ (n,L)) +* (b,a);
reconsider m = (0_ (n,L)) +* (b,a) as Function of (Bags n), the carrier of L ;
reconsider m = m as Function of (Bags n),L ;
reconsider m = m as Series of n,L ;
A1: b in Bags n by PRE_POLY:def_12;
 dom (b .--> a) = {b} by FUNCOP_1:13;
then A2: b in dom (b .--> a) by TARSKI:def_1;
dom (0_ (n,L)) = dom ((Bags n) --> (0. L)) by POLYNOM1:def_7
.= Bags n by FUNCOP_1:13 ;
then A3: m . b = ((0_ (n,L)) +* (b .--> a)) . b by A1, FUNCT_7:def_3
.= (b .--> a) . b by A2, FUNCT_4:13
.= a by FUNCOP_1:72 ;
percases ( m . b <> 0. L or m . b = 0. L ) ;
suppose m . b <> 0. L ; ::_thesis: coefficient (Monom (a,b)) = a
hence  coefficient (Monom (a,b)) = a by A3, Def5; ::_thesis: verum
end;
suppose m . b = 0. L ; ::_thesis: coefficient (Monom (a,b)) = a
hence  coefficient (Monom (a,b)) = a by A3, Th8; ::_thesis: verum
end;
end;
end;

theorem Th10: :: POLYNOM7:10
for X being set
for L being non trivial ZeroStr
for a being non zero Element of L
for b being bag of X holds term (Monom (a,b)) = b
proof
let n be set ; ::_thesis: for L being non trivial ZeroStr
for a being non zero Element of L
for b being bag of n holds term (Monom (a,b)) = b
let L be non trivial ZeroStr ; ::_thesis: for a being non zero Element of L
for b being bag of n holds term (Monom (a,b)) = b
let a be non zero Element of L; ::_thesis: for b being bag of n holds term (Monom (a,b)) = b
let b be bag of n; ::_thesis: term (Monom (a,b)) = b
set m = (0_ (n,L)) +* (b,a);
reconsider m = (0_ (n,L)) +* (b,a) as Function of (Bags n), the carrier of L ;
reconsider m = m as Function of (Bags n),L ;
reconsider m = m as Series of n,L ;
A1: b in Bags n by PRE_POLY:def_12;
 dom (b .--> a) = {b} by FUNCOP_1:13;
then A2: b in dom (b .--> a) by TARSKI:def_1;
dom (0_ (n,L)) = dom ((Bags n) --> (0. L)) by POLYNOM1:def_7
.= Bags n by FUNCOP_1:13 ;
then m . b = ((0_ (n,L)) +* (b .--> a)) . b by A1, FUNCT_7:def_3
.= (b .--> a) . b by A2, FUNCT_4:13
.= a by FUNCOP_1:72 ;
then  m . b <> 0. L ;
hence  term (Monom (a,b)) = b by Def5; ::_thesis: verum
end;

theorem :: POLYNOM7:11
for X being set
for L being non empty ZeroStr
for m being Monomial of X,L holds Monom ((coefficient m),(term m)) = m
proof
let X be set ; ::_thesis: for L being non empty ZeroStr
for m being Monomial of X,L holds Monom ((coefficient m),(term m)) = m
let L be non empty ZeroStr ; ::_thesis: for m being Monomial of X,L holds Monom ((coefficient m),(term m)) = m
let m be Monomial of X,L; ::_thesis: Monom ((coefficient m),(term m)) = m
A1: ( dom m = Bags X & dom (Monom ((coefficient m),(term m))) = Bags X ) by FUNCT_2:def_1;
percases ( Support m = {} or ex b being bag of X st Support m = {b} ) by Th6;
supposeA2: Support m = {} ; ::_thesis: Monom ((coefficient m),(term m)) = m
A3: now__::_thesis:_not_coefficient_m_<>_0._L
A4: term m is Element of Bags X by PRE_POLY:def_12;
assume  coefficient m <> 0. L ; ::_thesis: contradiction
hence  contradiction by A2, A4, POLYNOM1:def_3; ::_thesis: verum
end;
A5: m = 0_ (X,L) by A2, Th1;
set m9 = Monom ((coefficient m),(term m));
A6: dom (0_ (X,L)) = dom ((Bags X) --> (0. L)) by POLYNOM1:def_7
.= Bags X by FUNCOP_1:13 ;
 dom ((EmptyBag X) .--> (0. L)) = {(EmptyBag X)} by FUNCOP_1:13;
then A7: EmptyBag X in dom ((EmptyBag X) .--> (0. L)) by TARSKI:def_1;
A8: term m = EmptyBag X by A2, Def5;
then A9: (Monom ((coefficient m),(term m))) . (EmptyBag X) = ((0_ (X,L)) +* ((EmptyBag X) .--> (0. L))) . (EmptyBag X) by A3, A6, FUNCT_7:def_3
.= ((EmptyBag X) .--> (0. L)) . (EmptyBag X) by A7, FUNCT_4:13
.= 0. L by FUNCOP_1:72 ;
now__::_thesis:_for_x_being_set_st_x_in_Bags_X_holds_
m_._x_=_(Monom_((coefficient_m),(term_m)))_._x
let x be set ; ::_thesis: ( x in Bags X implies m . x = (Monom ((coefficient m),(term m))) . x )
assume  x in Bags X ; ::_thesis: m . x = (Monom ((coefficient m),(term m))) . x
then reconsider x9 = x as Element of Bags X ;
now__::_thesis:_(_(_x9_=_EmptyBag_X_&_(Monom_((coefficient_m),(term_m)))_._x9_=_0._L_)_or_(_x_<>_EmptyBag_X_&_(Monom_((coefficient_m),(term_m)))_._x9_=_0._L_)_)
percases ( x9 = EmptyBag X or x <> EmptyBag X ) ;
case x9 = EmptyBag X ; ::_thesis: (Monom ((coefficient m),(term m))) . x9 = 0. L
hence  (Monom ((coefficient m),(term m))) . x9 = 0. L by A9; ::_thesis: verum
end;
case x <> EmptyBag X ; ::_thesis: (Monom ((coefficient m),(term m))) . x9 = 0. L
then A10: not x9 in dom ((EmptyBag X) .--> (0. L)) by TARSKI:def_1;
(Monom ((coefficient m),(term m))) . x9 = ((0_ (X,L)) +* ((EmptyBag X) .--> (0. L))) . x9 by A8, A3, A6, FUNCT_7:def_3
.= (0_ (X,L)) . x9 by A10, FUNCT_4:11 ;
hence  (Monom ((coefficient m),(term m))) . x9 = 0. L by POLYNOM1:22; ::_thesis: verum
end;
end;
end;
hence  m . x = (Monom ((coefficient m),(term m))) . x by A5, POLYNOM1:22; ::_thesis: verum
end;
hence  Monom ((coefficient m),(term m)) = m by A1, FUNCT_1:2; ::_thesis: verum
end;
suppose ex b being bag of X st Support m = {b} ; ::_thesis: Monom ((coefficient m),(term m)) = m
then consider b being bag of X such that
A11: Support m = {b} ;
set a = m . b;
 dom (b .--> (m . b)) = {b} by FUNCOP_1:13;
then A12: b in dom (b .--> (m . b)) by TARSKI:def_1;
set m9 = Monom ((coefficient m),(term m));
A13: dom (0_ (X,L)) = dom ((Bags X) --> (0. L)) by POLYNOM1:def_7
.= Bags X by FUNCOP_1:13 ;
A14: b in Support m by A11, TARSKI:def_1;
then  m . b <> 0. L by POLYNOM1:def_3;
then A15: term m = b by Def5;
A16: now__::_thesis:_for_u_being_set_st_u_in_Support_(Monom_((coefficient_m),(term_m)))_holds_
u_in_{b}
let u be set ; ::_thesis: ( u in Support (Monom ((coefficient m),(term m))) implies u in {b} )
assume A17: u in Support (Monom ((coefficient m),(term m))) ; ::_thesis: u in {b}
then reconsider u9 = u as Element of Bags X ;
now__::_thesis:_(_u_<>_b_implies_(Monom_((coefficient_m),(term_m)))_._u9_=_0._L_)
assume  u <> b ; ::_thesis: (Monom ((coefficient m),(term m))) . u9 = 0. L
then A18: not u9 in dom (b .--> (m . b)) by TARSKI:def_1;
 b in dom (0_ (X,L)) by A13, PRE_POLY:def_12;
then (Monom ((coefficient m),(term m))) . u9 = ((0_ (X,L)) +* (b .--> (m . b))) . u9 by A15, FUNCT_7:def_3
.= (0_ (X,L)) . u9 by A18, FUNCT_4:11 ;
hence  (Monom ((coefficient m),(term m))) . u9 = 0. L by POLYNOM1:22; ::_thesis: verum
end;
hence  u in {b} by A17, POLYNOM1:def_3, TARSKI:def_1; ::_thesis: verum
end;
 b in Bags X by PRE_POLY:def_12;
then A19: (Monom ((coefficient m),(term m))) . b = ((0_ (X,L)) +* (b .--> (m . b))) . b by A15, A13, FUNCT_7:def_3
.= (b .--> (m . b)) . b by A12, FUNCT_4:13
.= m . b by FUNCOP_1:72 ;
now__::_thesis:_for_u_being_set_st_u_in_{b}_holds_
u_in_Support_(Monom_((coefficient_m),(term_m)))
let u be set ; ::_thesis: ( u in {b} implies u in Support (Monom ((coefficient m),(term m))) )
assume  u in {b} ; ::_thesis: u in Support (Monom ((coefficient m),(term m)))
then A20: u = b by TARSKI:def_1;
 (Monom ((coefficient m),(term m))) . b <> 0. L by A14, A19, POLYNOM1:def_3;
hence  u in Support (Monom ((coefficient m),(term m))) by A14, A20, POLYNOM1:def_3; ::_thesis: verum
end;
then A21: Support (Monom ((coefficient m),(term m))) = {b} by A16, TARSKI:1;
now__::_thesis:_for_x_being_set_st_x_in_Bags_X_holds_
m_._x_=_(Monom_((coefficient_m),(term_m)))_._x
let x be set ; ::_thesis: ( x in Bags X implies m . x = (Monom ((coefficient m),(term m))) . x )
assume  x in Bags X ; ::_thesis: m . x = (Monom ((coefficient m),(term m))) . x
then reconsider x9 = x as Element of Bags X ;
now__::_thesis:_(_(_x_=_b_&_(Monom_((coefficient_m),(term_m)))_._x9_=_m_._x9_)_or_(_x_<>_b_&_m_._x9_=_(Monom_((coefficient_m),(term_m)))_._x9_)_)
percases ( x = b or x <> b ) ;
case x = b ; ::_thesis: (Monom ((coefficient m),(term m))) . x9 = m . x9
hence  (Monom ((coefficient m),(term m))) . x9 = m . x9 by A19; ::_thesis: verum
end;
caseA22: x <> b ; ::_thesis: m . x9 = (Monom ((coefficient m),(term m))) . x9
then A23: not x in Support (Monom ((coefficient m),(term m))) by A21, TARSKI:def_1;
 not x in Support m by A11, A22, TARSKI:def_1;
hence m . x9 = 0. L by POLYNOM1:def_3
.= (Monom ((coefficient m),(term m))) . x9 by A23, POLYNOM1:def_3 ;
::_thesis: verum
end;
end;
end;
hence  m . x = (Monom ((coefficient m),(term m))) . x ; ::_thesis: verum
end;
hence  Monom ((coefficient m),(term m)) = m by A1, FUNCT_1:2; ::_thesis: verum
end;
end;
end;

theorem Th12: :: POLYNOM7:12
for n being Ordinal
for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for m being Monomial of n,L
for x being Function of n,L holds eval (m,x) = (coefficient m) * (eval ((term m),x))
proof
let n be Ordinal; ::_thesis: for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for m being Monomial of n,L
for x being Function of n,L holds eval (m,x) = (coefficient m) * (eval ((term m),x))
let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; ::_thesis: for m being Monomial of n,L
for x being Function of n,L holds eval (m,x) = (coefficient m) * (eval ((term m),x))
let m be Monomial of n,L; ::_thesis: for x being Function of n,L holds eval (m,x) = (coefficient m) * (eval ((term m),x))
let x be Function of n,L; ::_thesis: eval (m,x) = (coefficient m) * (eval ((term m),x))
consider y being FinSequence of the carrier of L such that
A1: len y = len (SgmX ((BagOrder n),(Support m))) and
A2: eval (m,x) = Sum y and
A3: for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((m * (SgmX ((BagOrder n),(Support m)))) /. i) * (eval ((((SgmX ((BagOrder n),(Support m))) /. i) @),x)) by POLYNOM2:def_4;
consider b being bag of n such that
A4: for b9 being bag of n st b9 <> b holds
m . b9 = 0. L by Def3;
now__::_thesis:_(_(_m_._b_<>_0._L_&_eval_(m,x)_=_(coefficient_m)_*_(eval_((term_m),x))_)_or_(_m_._b_=_0._L_&_eval_(m,x)_=_(coefficient_m)_*_(eval_((term_m),x))_)_)
percases ( m . b <> 0. L or m . b = 0. L ) ;
caseA5: m . b <> 0. L ; ::_thesis: eval (m,x) = (coefficient m) * (eval ((term m),x))
A6: for u being set st u in Support m holds
u in {b}
proof
let u be set ; ::_thesis: ( u in Support m implies u in {b} )
assume A7: u in Support m ; ::_thesis: u in {b}
assume A8: not u in {b} ; ::_thesis: contradiction
reconsider u = u as Element of Bags n by A7;
 u <> b by A8, TARSKI:def_1;
then  m . u = 0. L by A4;
hence  contradiction by A7, POLYNOM1:def_3; ::_thesis: verum
end;
A9: ( b in Bags n & dom m = Bags n ) by FUNCT_2:def_1, PRE_POLY:def_12;
reconsider sm = Support m as finite Subset of (Bags n) ;
set sg = SgmX ((BagOrder n),sm);
A10: BagOrder n linearly_orders sm by POLYNOM2:18;
 for u being set st u in {b} holds
u in Support m
proof
let u be set ; ::_thesis: ( u in {b} implies u in Support m )
assume A11: u in {b} ; ::_thesis: u in Support m
then  u = b by TARSKI:def_1;
then reconsider u = u as Element of Bags n by PRE_POLY:def_12;
 m . u <> 0. L by A5, A11, TARSKI:def_1;
hence  u in Support m by POLYNOM1:def_3; ::_thesis: verum
end;
then  Support m = {b} by A6, TARSKI:1;
then A12: rng (SgmX ((BagOrder n),sm)) = {b} by A10, PRE_POLY:def_2;
then A13: b in rng (SgmX ((BagOrder n),sm)) by TARSKI:def_1;
then A14: 1 in dom (SgmX ((BagOrder n),sm)) by FINSEQ_3:31;
then A15: (SgmX ((BagOrder n),sm)) . 1 in rng (SgmX ((BagOrder n),sm)) by FUNCT_1:3;
then  (SgmX ((BagOrder n),sm)) . 1 = b by A12, TARSKI:def_1;
then  1 in dom (m * (SgmX ((BagOrder n),sm))) by A14, A9, FUNCT_1:11;
then A16: (m * (SgmX ((BagOrder n),sm))) /. 1 = (m * (SgmX ((BagOrder n),sm))) . 1 by PARTFUN1:def_6
.= m . ((SgmX ((BagOrder n),sm)) . 1) by A14, FUNCT_1:13
.= m . b by A12, A15, TARSKI:def_1
.= coefficient m by A5, Def5 ;
A17: for u being set st u in dom (SgmX ((BagOrder n),sm)) holds
u in {1}
proof
let u be set ; ::_thesis: ( u in dom (SgmX ((BagOrder n),sm)) implies u in {1} )
assume A18: u in dom (SgmX ((BagOrder n),sm)) ; ::_thesis: u in {1}
assume A19: not u in {1} ; ::_thesis: contradiction
reconsider u = u as Element of NAT by A18;
 (SgmX ((BagOrder n),sm)) /. u = (SgmX ((BagOrder n),sm)) . u by A18, PARTFUN1:def_6;
then A20: (SgmX ((BagOrder n),sm)) /. u in rng (SgmX ((BagOrder n),sm)) by A18, FUNCT_1:3;
A21: u <> 1 by A19, TARSKI:def_1;
A22: 1 < u
proof
consider k being Nat such that
A23: dom (SgmX ((BagOrder n),sm)) = Seg k by FINSEQ_1:def_2;
 Seg k =  {  l where l is Element of NAT : ( 1 <= l & l <= k )  }  by FINSEQ_1:def_1;
then  ex m9 being Element of NAT st
( m9 = u & 1 <= m9 & m9 <= k ) by A18, A23;
hence  1 < u by A21, XXREAL_0:1; ::_thesis: verum
end;
 (SgmX ((BagOrder n),sm)) /. 1 = (SgmX ((BagOrder n),sm)) . 1 by A13, A18, FINSEQ_3:31, PARTFUN1:def_6;
then  (SgmX ((BagOrder n),sm)) /. 1 in rng (SgmX ((BagOrder n),sm)) by A14, FUNCT_1:3;
then (SgmX ((BagOrder n),sm)) /. 1 = b by A12, TARSKI:def_1
.= (SgmX ((BagOrder n),sm)) /. u by A12, A20, TARSKI:def_1 ;
hence  contradiction by A10, A14, A18, A22, PRE_POLY:def_2; ::_thesis: verum
end;
 for u being set st u in {1} holds
u in dom (SgmX ((BagOrder n),sm)) by A14, TARSKI:def_1;
then A24: dom (SgmX ((BagOrder n),sm)) = Seg 1 by A17, FINSEQ_1:2, TARSKI:1;
then A25: 1 in dom (SgmX ((BagOrder n),sm)) by FINSEQ_1:2, TARSKI:def_1;
 (SgmX ((BagOrder n),sm)) /. 1 = (SgmX ((BagOrder n),sm)) . 1 by A14, PARTFUN1:def_6;
then  (SgmX ((BagOrder n),sm)) /. 1 in rng (SgmX ((BagOrder n),sm)) by A25, FUNCT_1:3;
then A26: (SgmX ((BagOrder n),sm)) /. 1 = b by A12, TARSKI:def_1;
A27: len (SgmX ((BagOrder n),sm)) = 1 by A24, FINSEQ_1:def_3;
dom y = Seg (len y) by FINSEQ_1:def_3
.= dom (SgmX ((BagOrder n),sm)) by A1, FINSEQ_1:def_3 ;
then y . 1 = y /. 1 by A25, PARTFUN1:def_6
.= ((m * (SgmX ((BagOrder n),sm))) /. 1) * (eval ((((SgmX ((BagOrder n),sm)) /. 1) @),x)) by A1, A3, A27
.= ((m * (SgmX ((BagOrder n),sm))) /. 1) * (eval (b,x)) by A26, POLYNOM2:def_3 ;
then  y = <*((coefficient m) * (eval (b,x)))*> by A1, A27, A16, FINSEQ_1:40;
hence  eval (m,x) = (coefficient m) * (eval (b,x)) by A2, RLVECT_1:44
.= (coefficient m) * (eval ((term m),x)) by A5, Def5 ;
::_thesis: verum
end;
caseA28: m . b = 0. L ; ::_thesis: eval (m,x) = (coefficient m) * (eval ((term m),x))
A29: Support m = {}
proof
assume  Support m <> {} ; ::_thesis: contradiction
then reconsider sm = Support m as non empty Subset of (Bags n) ;
set c = the Element of sm;
 m . the Element of sm <> 0. L by POLYNOM1:def_3;
hence  contradiction by A4, A28; ::_thesis: verum
end;
then  ( term m = EmptyBag n & m . (EmptyBag n) = 0. L ) by Def5, POLYNOM1:def_3;
then A30: (coefficient m) * (eval ((term m),x)) = 0. L by VECTSP_1:7;
consider y being FinSequence of the carrier of L such that
A31: len y = len (SgmX ((BagOrder n),(Support m))) and
A32: eval (m,x) = Sum y and
 for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((m * (SgmX ((BagOrder n),(Support m)))) /. i) * (eval ((((SgmX ((BagOrder n),(Support m))) /. i) @),x)) by POLYNOM2:def_4;
 BagOrder n linearly_orders Support m by POLYNOM2:18;
then  rng (SgmX ((BagOrder n),(Support m))) = {} by A29, PRE_POLY:def_2;
then  SgmX ((BagOrder n),(Support m)) = {} by RELAT_1:41;
then  y = <*> the carrier of L by A31;
hence  eval (m,x) = (coefficient m) * (eval ((term m),x)) by A30, A32, RLVECT_1:43; ::_thesis: verum
end;
end;
end;
hence  eval (m,x) = (coefficient m) * (eval ((term m),x)) ; ::_thesis: verum
end;

theorem :: POLYNOM7:13
for n being Ordinal
for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for a being Element of L
for b being bag of n
for x being Function of n,L holds eval ((Monom (a,b)),x) = a * (eval (b,x))
proof
let n be Ordinal; ::_thesis: for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for a being Element of L
for b being bag of n
for x being Function of n,L holds eval ((Monom (a,b)),x) = a * (eval (b,x))
let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; ::_thesis: for a being Element of L
for b being bag of n
for x being Function of n,L holds eval ((Monom (a,b)),x) = a * (eval (b,x))
let a be Element of L; ::_thesis: for b being bag of n
for x being Function of n,L holds eval ((Monom (a,b)),x) = a * (eval (b,x))
let b be bag of n; ::_thesis: for x being Function of n,L holds eval ((Monom (a,b)),x) = a * (eval (b,x))
let x be Function of n,L; ::_thesis: eval ((Monom (a,b)),x) = a * (eval (b,x))
set m = Monom (a,b);
now__::_thesis:_(_(_a_<>_0._L_&_eval_((Monom_(a,b)),x)_=_a_*_(eval_(b,x))_)_or_(_a_=_0._L_&_eval_((Monom_(a,b)),x)_=_a_*_(eval_(b,x))_)_)
percases ( a <> 0. L or a = 0. L ) ;
case a <> 0. L ; ::_thesis: eval ((Monom (a,b)),x) = a * (eval (b,x))
then A1: not a is zero by STRUCT_0:def_12;
thus  eval ((Monom (a,b)),x) = (coefficient (Monom (a,b))) * (eval ((term (Monom (a,b))),x)) by Th12
.= a * (eval ((term (Monom (a,b))),x)) by Th9
.= a * (eval (b,x)) by A1, Th10 ; ::_thesis: verum
end;
caseA2: a = 0. L ; ::_thesis: eval ((Monom (a,b)),x) = a * (eval (b,x))
 for b9 being bag of n holds (Monom (a,b)) . b9 = 0. L
proof
let b9 be bag of n; ::_thesis: (Monom (a,b)) . b9 = 0. L
now__::_thesis:_(_(_b9_=_b_&_(Monom_(a,b))_._b9_=_0._L_)_or_(_b9_<>_b_&_(Monom_(a,b))_._b9_=_0._L_)_)
percases ( b9 = b or b9 <> b ) ;
caseA3: b9 = b ; ::_thesis: (Monom (a,b)) . b9 = 0. L
A4: b in Bags n by PRE_POLY:def_12;
 dom (b .--> a) = {b} by FUNCOP_1:13;
then A5: b in dom (b .--> a) by TARSKI:def_1;
dom (0_ (n,L)) = dom ((Bags n) --> (0. L)) by POLYNOM1:def_7
.= Bags n by FUNCOP_1:13 ;
then  Monom (a,b) = (0_ (n,L)) +* (b .--> a) by A4, FUNCT_7:def_3;
hence (Monom (a,b)) . b9 = (b .--> a) . b by A3, A5, FUNCT_4:13
.= 0. L by A2, FUNCOP_1:72 ;
::_thesis: verum
end;
case b9 <> b ; ::_thesis: (Monom (a,b)) . b9 = 0. L
hence (Monom (a,b)) . b9 = (0_ (n,L)) . b9 by FUNCT_7:32
.= 0. L by POLYNOM1:22 ;
::_thesis: verum
end;
end;
end;
hence  (Monom (a,b)) . b9 = 0. L ; ::_thesis: verum
end;
then A6: (Monom (a,b)) . (term (Monom (a,b))) = 0. L ;
thus  eval ((Monom (a,b)),x) = (coefficient (Monom (a,b))) * (eval ((term (Monom (a,b))),x)) by Th12
.= 0. L by A6, VECTSP_1:7
.= a * (eval (b,x)) by A2, VECTSP_1:7 ; ::_thesis: verum
end;
end;
end;
hence  eval ((Monom (a,b)),x) = a * (eval (b,x)) ; ::_thesis: verum
end;

begin

definition
let X be set ;
let L be non empty ZeroStr ;
let p be Series of X,L;
attrp is Constant  means :Def7: :: POLYNOM7:def 7
 for b being bag of X st b <> EmptyBag X holds
p . b = 0. L;
end;

:: deftheorem Def7 defines Constant POLYNOM7:def_7_:_
 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 );

registration
let X be set ;
let L be non empty ZeroStr ;
cluster Relation-like Bags X -defined the carrier of L -valued Function-like V18( Bags X, the carrier of L) Constant for Element of bool [:(Bags X), the carrier of L:];
existence
 ex b1 being Series of X,L st b1 is Constant
proof
set c = 0_ (X,L);
take  0_ (X,L) ; ::_thesis: 0_ (X,L) is Constant
 for b being bag of X st b <> EmptyBag X holds
(0_ (X,L)) . b = 0. L by POLYNOM1:22;
hence  0_ (X,L) is Constant by Def7; ::_thesis: verum
end;
end;

definition
let X be set ;
let L be non empty ZeroStr ;
mode ConstPoly of X,L is Constant Series of X,L;
end;

registration
let X be set ;
let L be non empty ZeroStr ;
cluster Function-like V18( Bags X, the carrier of L) Constant  ->  monomial-like for Element of bool [:(Bags X), the carrier of L:];
coherence
 for b1 being Series of X,L st b1 is Constant holds
b1 is monomial-like
proof
let p be Series of X,L; ::_thesis: ( p is Constant implies p is monomial-like )
assume  p is Constant ; ::_thesis: p is monomial-like
then  for b being bag of X st b <> EmptyBag X holds
p . b = 0. L by Def7;
hence  p is monomial-like by Def3; ::_thesis: verum
end;
end;

theorem Th14: :: POLYNOM7:14
for X being set
for L being non empty ZeroStr
for p being Series of X,L holds
( p is ConstPoly of X,L iff ( p = 0_ (X,L) or Support p = {(EmptyBag X)} ) )
proof
let n be set ; ::_thesis: for L being non empty ZeroStr
for p being Series of n,L holds
( p is ConstPoly of n,L iff ( p = 0_ (n,L) or Support p = {(EmptyBag n)} ) )
let L be non empty ZeroStr ; ::_thesis: for p being Series of n,L holds
( p is ConstPoly of n,L iff ( p = 0_ (n,L) or Support p = {(EmptyBag n)} ) )
let p be Series of n,L; ::_thesis: ( p is ConstPoly of n,L iff ( p = 0_ (n,L) or Support p = {(EmptyBag n)} ) )
A1: now__::_thesis:_(_not_p_is_ConstPoly_of_n,L_or_Support_p_=_{(EmptyBag_n)}_or_p_=_0__(n,L)_)
assume A2: p is ConstPoly of n,L ; ::_thesis: ( Support p = {(EmptyBag n)} or p = 0_ (n,L) )
A3: for u being set st u in Support p holds
u in {(EmptyBag n)}
proof
let u be set ; ::_thesis: ( u in Support p implies u in {(EmptyBag n)} )
assume A4: u in Support p ; ::_thesis: u in {(EmptyBag n)}
then reconsider u = u as Element of Bags n ;
reconsider u9 = u as bag of n ;
 p . u9 <> 0. L by A4, POLYNOM1:def_3;
then  u9 = EmptyBag n by A2, Def7;
hence  u in {(EmptyBag n)} by TARSKI:def_1; ::_thesis: verum
end;
thus  ( Support p = {(EmptyBag n)} or p = 0_ (n,L) ) ::_thesis: verum
proof
assume A5: not Support p = {(EmptyBag n)} ; ::_thesis: p = 0_ (n,L)
A6: not EmptyBag n in Support p
proof
assume  EmptyBag n in Support p ; ::_thesis: contradiction
then  for u being set st u in {(EmptyBag n)} holds
u in Support p by TARSKI:def_1;
hence  contradiction by A3, A5, TARSKI:1; ::_thesis: verum
end;
A7: Support p = {}
proof
set v = the Element of Support p;
assume  Support p <> {} ; ::_thesis: contradiction
then  ( the Element of Support p in Support p & the Element of Support p in {(EmptyBag n)} ) by A3;
hence  contradiction by A6, TARSKI:def_1; ::_thesis: verum
end;
A8: for b being bag of n holds p . b = 0. L
proof
let b be bag of n; ::_thesis: p . b = 0. L
A9: b is Element of Bags n by PRE_POLY:def_12;
assume  p . b <> 0. L ; ::_thesis: contradiction
hence  contradiction by A7, A9, POLYNOM1:def_3; ::_thesis: verum
end;
A10: for u being set st u in rng p holds
u in {(0. L)}
proof
let u be set ; ::_thesis: ( u in rng p implies u in {(0. L)} )
assume  u in rng p ; ::_thesis: u in {(0. L)}
then consider x being set  such that
A11: x in dom p and
A12: p . x = u by FUNCT_1:def_3;
 x is bag of n by A11;
then  u = 0. L by A8, A12;
hence  u in {(0. L)} by TARSKI:def_1; ::_thesis: verum
end;
A13: dom p = Bags n by FUNCT_2:def_1;
 for u being set st u in {(0. L)} holds
u in rng p
proof
set b = the bag of n;
let u be set ; ::_thesis: ( u in {(0. L)} implies u in rng p )
assume  u in {(0. L)} ; ::_thesis: u in rng p
then  u = 0. L by TARSKI:def_1;
then A14: p . the bag of n = u by A8;
 the bag of n in dom p by A13, PRE_POLY:def_12;
hence  u in rng p by A14, FUNCT_1:def_3; ::_thesis: verum
end;
then  rng p = {(0. L)} by A10, TARSKI:1;
then  p = (Bags n) --> (0. L) by A13, FUNCOP_1:9;
hence  p = 0_ (n,L) by POLYNOM1:def_7; ::_thesis: verum
end;
end;
now__::_thesis:_(_(_p_=_0__(n,L)_or_Support_p_=_{(EmptyBag_n)}_)_implies_p_is_ConstPoly_of_n,L_)
assume A15: ( p = 0_ (n,L) or Support p = {(EmptyBag n)} ) ; ::_thesis: p is ConstPoly of n,L
percases ( p = 0_ (n,L) or Support p = {(EmptyBag n)} ) by A15;
suppose p = 0_ (n,L) ; ::_thesis: p is ConstPoly of n,L
then  for b being bag of n st b <> EmptyBag n holds
p . b = 0. L by POLYNOM1:22;
hence  p is ConstPoly of n,L by Def7; ::_thesis: verum
end;
supposeA16: Support p = {(EmptyBag n)} ; ::_thesis: p is ConstPoly of n,L
 for b being bag of n st b <> EmptyBag n holds
p . b = 0. L
proof
let b be bag of n; ::_thesis: ( b <> EmptyBag n implies p . b = 0. L )
assume A17: b <> EmptyBag n ; ::_thesis: p . b = 0. L
reconsider b = b as Element of Bags n by PRE_POLY:def_12;
 not b in Support p by A16, A17, TARSKI:def_1;
hence  p . b = 0. L by POLYNOM1:def_3; ::_thesis: verum
end;
hence  p is ConstPoly of n,L by Def7; ::_thesis: verum
end;
end;
end;
hence  ( p is ConstPoly of n,L iff ( p = 0_ (n,L) or Support p = {(EmptyBag n)} ) ) by A1; ::_thesis: verum
end;

registration
let X be set ;
let L be non empty ZeroStr ;
cluster 0_ (X,L) ->  Constant ;
coherence
 0_ (X,L) is Constant
proof
 for b being bag of X st b <> EmptyBag X holds
(0_ (X,L)) . b = 0. L by POLYNOM1:22;
hence  0_ (X,L) is Constant by Def7; ::_thesis: verum
end;
end;

registration
let X be set ;
let L be non empty well-unital doubleLoopStr ;
cluster 1_ (X,L) ->  Constant ;
coherence
 1_ (X,L) is Constant
proof
 for b being bag of X st b <> EmptyBag X holds
(1_ (X,L)) . b = 0. L by POLYNOM1:25;
hence  1_ (X,L) is Constant by Def7; ::_thesis: verum
end;
end;

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) )
proof
let n be set ; ::_thesis: for L being non empty ZeroStr
for c being ConstPoly of n,L holds
( term c = EmptyBag n & coefficient c = c . (EmptyBag n) )
let L be non empty ZeroStr ; ::_thesis: for c being ConstPoly of n,L holds
( term c = EmptyBag n & coefficient c = c . (EmptyBag n) )
let c be ConstPoly of n,L; ::_thesis: ( term c = EmptyBag n & coefficient c = c . (EmptyBag n) )
set eb = EmptyBag n;
A1: now__::_thesis:_(_(_c_._(EmptyBag_n)_<>_0._L_&_term_c_=_EmptyBag_n_)_or_(_c_._(EmptyBag_n)_=_0._L_&_term_c_=_EmptyBag_n_)_)
percases ( c . (EmptyBag n) <> 0. L or c . (EmptyBag n) = 0. L ) ;
case c . (EmptyBag n) <> 0. L ; ::_thesis: term c = EmptyBag n
hence  term c = EmptyBag n by Def5; ::_thesis: verum
end;
caseA2: c . (EmptyBag n) = 0. L ; ::_thesis: term c = EmptyBag n
 Support c = {}
proof
set u = the Element of Support c;
assume A3: Support c <> {} ; ::_thesis: contradiction
then  the Element of Support c in Support c ;
then reconsider u = the Element of Support c as Element of Bags n ;
 c . u <> 0. L by A3, POLYNOM1:def_3;
hence  contradiction by A2, Def7; ::_thesis: verum
end;
hence  term c = EmptyBag n by Def5; ::_thesis: verum
end;
end;
end;
hence  term c = EmptyBag n ; ::_thesis: coefficient c = c . (EmptyBag n)
thus  coefficient c = c . (EmptyBag n) by A1; ::_thesis: verum
end;

theorem Th15: :: POLYNOM7:15
for X being set
for L being non empty ZeroStr
for c being ConstPoly of X,L holds
( Support c = {} or Support c = {(EmptyBag X)} )
proof
let X be set ; ::_thesis: for L being non empty ZeroStr
for c being ConstPoly of X,L holds
( Support c = {} or Support c = {(EmptyBag X)} )
let L be non empty ZeroStr ; ::_thesis: for c being ConstPoly of X,L holds
( Support c = {} or Support c = {(EmptyBag X)} )
let c be ConstPoly of X,L; ::_thesis: ( Support c = {} or Support c = {(EmptyBag X)} )
assume  Support c <> {} ; ::_thesis: Support c = {(EmptyBag X)}
hence  Support c = {(term c)} by Th7
.= {(EmptyBag X)} by Lm2 ;
::_thesis: verum
end;

theorem :: POLYNOM7:16
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) ) by Lm2;

definition
let X be set ;
let L be non empty ZeroStr ;
let a be Element of L;
funca | (X,L) ->  Series of X,L equals :: POLYNOM7:def 8
(0_ (X,L)) +* ((EmptyBag X),a);
coherence
 (0_ (X,L)) +* ((EmptyBag X),a) is Series of X,L ;
end;

:: deftheorem  defines | POLYNOM7:def_8_:_
 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);

registration
let X be set ;
let L be non empty ZeroStr ;
let a be Element of L;
clustera | (X,L) ->  Constant ;
coherence
 a | (X,L) is Constant
proof
set Z = 0_ (X,L);
set O = (0_ (X,L)) +* ((EmptyBag X),a);
reconsider O = (0_ (X,L)) +* ((EmptyBag X),a) as Function of (Bags X), the carrier of L ;
reconsider O9 = O as Function of (Bags X),L ;
reconsider O9 = O9 as Series of X,L ;
now__::_thesis:_for_b_being_bag_of_X_st_b_<>_EmptyBag_X_holds_
O9_._b_=_0._L
let b be bag of X; ::_thesis: ( b <> EmptyBag X implies O9 . b = 0. L )
dom (0_ (X,L)) = dom ((Bags X) --> (0. L)) by POLYNOM1:def_7
.= Bags X by FUNCOP_1:13 ;
then A1: O9 = (0_ (X,L)) +* ((EmptyBag X) .--> a) by FUNCT_7:def_3;
assume  b <> EmptyBag X ; ::_thesis: O9 . b = 0. L
then  not b in dom ((EmptyBag X) .--> a) by TARSKI:def_1;
hence O9 . b = (0_ (X,L)) . b by A1, FUNCT_4:11
.= 0. L by POLYNOM1:22 ;
::_thesis: verum
end;
hence  a | (X,L) is Constant by Def7; ::_thesis: verum
end;
end;

Lm3:  for X being set
for L being non empty ZeroStr holds (0. L) | (X,L) = 0_ (X,L)
proof
let X be set ; ::_thesis: for L being non empty ZeroStr holds (0. L) | (X,L) = 0_ (X,L)
let L be non empty ZeroStr ; ::_thesis: (0. L) | (X,L) = 0_ (X,L)
set o1 = (0. L) | (X,L);
set o2 = 0_ (X,L);
A1: now__::_thesis:_for_x_being_set_st_x_in_Bags_X_holds_
((0._L)_|_(X,L))_._x_=_(0__(X,L))_._x
set m = (0_ (X,L)) +* ((EmptyBag X),(0. L));
let x be set ; ::_thesis: ( x in Bags X implies ((0. L) | (X,L)) . b1 = (0_ (X,L)) . b1 )
reconsider m = (0_ (X,L)) +* ((EmptyBag X),(0. L)) as Function of (Bags X), the carrier of L ;
reconsider m = m as Function of (Bags X),L ;
reconsider m = m as Series of X,L ;
assume  x in Bags X ; ::_thesis: ((0. L) | (X,L)) . b1 = (0_ (X,L)) . b1
then reconsider x9 = x as bag of X ;
A2: dom (0_ (X,L)) = dom ((Bags X) --> (0. L)) by POLYNOM1:def_7
.= Bags X by FUNCOP_1:13 ;
then A3: m = (0_ (X,L)) +* ((EmptyBag X) .--> (0. L)) by FUNCT_7:def_3;
 dom ((EmptyBag X) .--> (0. L)) = {(EmptyBag X)} by FUNCOP_1:13;
then A4: EmptyBag X in dom ((EmptyBag X) .--> (0. L)) by TARSKI:def_1;
A5: m . (EmptyBag X) = ((0_ (X,L)) +* ((EmptyBag X) .--> (0. L))) . (EmptyBag X) by A2, FUNCT_7:def_3
.= ((EmptyBag X) .--> (0. L)) . (EmptyBag X) by A4, FUNCT_4:13
.= 0. L by FUNCOP_1:72 ;
percases ( x9 = EmptyBag X or x9 <> EmptyBag X ) ;
suppose x9 = EmptyBag X ; ::_thesis: ((0. L) | (X,L)) . b1 = (0_ (X,L)) . b1
hence  ((0. L) | (X,L)) . x = (0_ (X,L)) . x by A5, POLYNOM1:22; ::_thesis: verum
end;
suppose x9 <> EmptyBag X ; ::_thesis: ((0. L) | (X,L)) . b1 = (0_ (X,L)) . b1
then  not x9 in dom ((EmptyBag X) .--> (0. L)) by TARSKI:def_1;
hence  ((0. L) | (X,L)) . x = (0_ (X,L)) . x by A3, FUNCT_4:11; ::_thesis: verum
end;
end;
end;
 ( Bags X = dom ((0. L) | (X,L)) & Bags X = dom (0_ (X,L)) ) by FUNCT_2:def_1;
hence  (0. L) | (X,L) = 0_ (X,L) by A1, FUNCT_1:2; ::_thesis: verum
end;

theorem :: POLYNOM7:17
for X being set
for L being non empty ZeroStr
for p being Series of X,L holds
( p is ConstPoly of X,L iff ex a being Element of L st p = a | (X,L) )
proof
let X be set ; ::_thesis: for L being non empty ZeroStr
for p being Series of X,L holds
( p is ConstPoly of X,L iff ex a being Element of L st p = a | (X,L) )
let L be non empty ZeroStr ; ::_thesis: for p being Series of X,L holds
( p is ConstPoly of X,L iff ex a being Element of L st p = a | (X,L) )
let p be Series of X,L; ::_thesis: ( p is ConstPoly of X,L iff ex a being Element of L st p = a | (X,L) )
now__::_thesis:_(_p_is_ConstPoly_of_X,L_implies_ex_a_being_Element_of_L_st_p_=_a_|_(X,L)_)
assume A1: p is ConstPoly of X,L ; ::_thesis: ex a being Element of L st p = a | (X,L)
now__::_thesis:_(_(_p_=_0__(X,L)_&_ex_a_being_Element_of_L_st_p_=_a_|_(X,L)_)_or_(_Support_p_=_{(EmptyBag_X)}_&_ex_a_being_Element_of_L_st_p_=_a_|_(X,L)_)_)
percases ( p = 0_ (X,L) or Support p = {(EmptyBag X)} ) by A1, Th14;
case p = 0_ (X,L) ; ::_thesis: ex a being Element of L st p = a | (X,L)
then  p = (0. L) | (X,L) by Lm3;
hence  ex a being Element of L st p = a | (X,L) ; ::_thesis: verum
end;
caseA2: Support p = {(EmptyBag X)} ; ::_thesis: ex a being Element of L st p = a | (X,L)
set q = (0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X)));
A3: now__::_thesis:_for_x_being_set_st_x_in_Bags_X_holds_
p_._x_=_((0__(X,L))_+*_((EmptyBag_X),(p_._(EmptyBag_X))))_._x
let x be set ; ::_thesis: ( x in Bags X implies p . x = ((0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X)))) . x )
assume  x in Bags X ; ::_thesis: p . x = ((0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X)))) . x
then reconsider x9 = x as bag of X ;
A4: dom (0_ (X,L)) = dom ((Bags X) --> (0. L)) by POLYNOM1:def_7
.= Bags X by FUNCOP_1:13 ;
then A5: (0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X))) = (0_ (X,L)) +* ((EmptyBag X) .--> (p . (EmptyBag X))) by FUNCT_7:def_3;
 dom ((EmptyBag X) .--> (p . (EmptyBag X))) = {(EmptyBag X)} by FUNCOP_1:13;
then A6: EmptyBag X in dom ((EmptyBag X) .--> (p . (EmptyBag X))) by TARSKI:def_1;
A7: ((0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X)))) . (EmptyBag X) = ((0_ (X,L)) +* ((EmptyBag X) .--> (p . (EmptyBag X)))) . (EmptyBag X) by A4, FUNCT_7:def_3
.= ((EmptyBag X) .--> (p . (EmptyBag X))) . (EmptyBag X) by A6, FUNCT_4:13
.= p . (EmptyBag X) by FUNCOP_1:72 ;
now__::_thesis:_(_(_x9_=_EmptyBag_X_&_p_._x_=_((0__(X,L))_+*_((EmptyBag_X),(p_._(EmptyBag_X))))_._x_)_or_(_x9_<>_EmptyBag_X_&_p_._x_=_((0__(X,L))_+*_((EmptyBag_X),(p_._(EmptyBag_X))))_._x_)_)
percases ( x9 = EmptyBag X or x9 <> EmptyBag X ) ;
case x9 = EmptyBag X ; ::_thesis: p . x = ((0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X)))) . x
hence  p . x = ((0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X)))) . x by A7; ::_thesis: verum
end;
caseA8: x9 <> EmptyBag X ; ::_thesis: p . x = ((0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X)))) . x
A9: x9 is Element of Bags X by PRE_POLY:def_12;
 not x9 in Support p by A2, A8, TARSKI:def_1;
then A10: p . x9 = 0. L by A9, POLYNOM1:def_3;
 not x9 in dom ((EmptyBag X) .--> (p . (EmptyBag X))) by A8, TARSKI:def_1;
then  ((0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X)))) . x9 = (0_ (X,L)) . x9 by A5, FUNCT_4:11;
hence  p . x = ((0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X)))) . x by A10, POLYNOM1:22; ::_thesis: verum
end;
end;
end;
hence  p . x = ((0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X)))) . x ; ::_thesis: verum
end;
A11: Bags X = dom ((0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X)))) by FUNCT_2:def_1;
 ( (0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X))) = (p . (EmptyBag X)) | (X,L) & Bags X = dom p ) by FUNCT_2:def_1;
hence  ex a being Element of L st p = a | (X,L) by A11, A3, FUNCT_1:2; ::_thesis: verum
end;
end;
end;
hence  ex a being Element of L st p = a | (X,L) ; ::_thesis: verum
end;
hence  ( p is ConstPoly of X,L iff ex a being Element of L st p = a | (X,L) ) ; ::_thesis: verum
end;

theorem Th18: :: POLYNOM7:18
for X being set
for L being non empty multLoopStr_0
for a being Element of L holds
( (a | (X,L)) . (EmptyBag X) = a & ( for b being bag of X st b <> EmptyBag X holds
(a | (X,L)) . b = 0. L ) )
proof
let n be set ; ::_thesis: for L being non empty multLoopStr_0
for a being Element of L holds
( (a | (n,L)) . (EmptyBag n) = a & ( for b being bag of n st b <> EmptyBag n holds
(a | (n,L)) . b = 0. L ) )
let L be non empty multLoopStr_0 ; ::_thesis: for a being Element of L holds
( (a | (n,L)) . (EmptyBag n) = a & ( for b being bag of n st b <> EmptyBag n holds
(a | (n,L)) . b = 0. L ) )
let a be Element of L; ::_thesis: ( (a | (n,L)) . (EmptyBag n) = a & ( for b being bag of n st b <> EmptyBag n holds
(a | (n,L)) . b = 0. L ) )
set Z = 0_ (n,L);
A1: 0_ (n,L) = (Bags n) --> (0. L) by POLYNOM1:def_7;
then  dom (0_ (n,L)) = Bags n by FUNCOP_1:13;
hence  (a | (n,L)) . (EmptyBag n) = a by FUNCT_7:31; ::_thesis: for b being bag of n st b <> EmptyBag n holds
(a | (n,L)) . b = 0. L
let b be bag of n; ::_thesis: ( b <> EmptyBag n implies (a | (n,L)) . b = 0. L )
A2: b in Bags n by PRE_POLY:def_12;
assume  b <> EmptyBag n ; ::_thesis: (a | (n,L)) . b = 0. L
hence (a | (n,L)) . b = (0_ (n,L)) . b by FUNCT_7:32
.= 0. L by A1, A2, FUNCOP_1:7 ;
::_thesis: verum
end;

theorem :: POLYNOM7:19
for X being set
for L being non empty ZeroStr holds (0. L) | (X,L) = 0_ (X,L) by Lm3;

theorem :: POLYNOM7:20
for X being set
for L being non empty well-unital multLoopStr_0 holds (1. L) | (X,L) = 1_ (X,L)
proof
let X be set ; ::_thesis: for L being non empty well-unital multLoopStr_0 holds (1. L) | (X,L) = 1_ (X,L)
let L be non empty well-unital multLoopStr_0 ; ::_thesis: (1. L) | (X,L) = 1_ (X,L)
set o1 = (1. L) | (X,L);
set o2 = 1_ (X,L);
A1: now__::_thesis:_for_x_being_set_st_x_in_Bags_X_holds_
((1._L)_|_(X,L))_._x_=_(1__(X,L))_._x
set m = (0_ (X,L)) +* ((EmptyBag X),(1. L));
let x be set ; ::_thesis: ( x in Bags X implies ((1. L) | (X,L)) . b1 = (1_ (X,L)) . b1 )
reconsider m = (0_ (X,L)) +* ((EmptyBag X),(1. L)) as Function of (Bags X), the carrier of L ;
reconsider m = m as Function of (Bags X),L ;
reconsider m = m as Series of X,L ;
assume  x in Bags X ; ::_thesis: ((1. L) | (X,L)) . b1 = (1_ (X,L)) . b1
then reconsider x9 = x as bag of X ;
A2: dom (0_ (X,L)) = dom ((Bags X) --> (0. L)) by POLYNOM1:def_7
.= Bags X by FUNCOP_1:13 ;
then A3: m = (0_ (X,L)) +* ((EmptyBag X) .--> (1. L)) by FUNCT_7:def_3;
 dom ((EmptyBag X) .--> (1. L)) = {(EmptyBag X)} by FUNCOP_1:13;
then A4: EmptyBag X in dom ((EmptyBag X) .--> (1. L)) by TARSKI:def_1;
A5: m . (EmptyBag X) = ((0_ (X,L)) +* ((EmptyBag X) .--> (1. L))) . (EmptyBag X) by A2, FUNCT_7:def_3
.= ((EmptyBag X) .--> (1. L)) . (EmptyBag X) by A4, FUNCT_4:13
.= 1. L by FUNCOP_1:72 ;
percases ( x9 = EmptyBag X or x9 <> EmptyBag X ) ;
suppose x9 = EmptyBag X ; ::_thesis: ((1. L) | (X,L)) . b1 = (1_ (X,L)) . b1
hence  ((1. L) | (X,L)) . x = (1_ (X,L)) . x by A5, POLYNOM1:25; ::_thesis: verum
end;
supposeA6: x9 <> EmptyBag X ; ::_thesis: ((1. L) | (X,L)) . b1 = (1_ (X,L)) . b1
then  not x9 in dom ((EmptyBag X) .--> (1. L)) by TARSKI:def_1;
then m . x9 = (0_ (X,L)) . x9 by A3, FUNCT_4:11
.= 0. L by POLYNOM1:22
.= (1_ (X,L)) . x9 by A6, POLYNOM1:25 ;
hence  ((1. L) | (X,L)) . x = (1_ (X,L)) . x ; ::_thesis: verum
end;
end;
end;
 ( Bags X = dom ((1. L) | (X,L)) & Bags X = dom (1_ (X,L)) ) by FUNCT_2:def_1;
hence  (1. L) | (X,L) = 1_ (X,L) by A1, FUNCT_1:2; ::_thesis: verum
end;

theorem :: POLYNOM7:21
for X being set
for L being non empty ZeroStr
for a, b being Element of L holds
( a | (X,L) = b | (X,L) iff a = b )
proof
let X be set ; ::_thesis: for L being non empty ZeroStr
for a, b being Element of L holds
( a | (X,L) = b | (X,L) iff a = b )
let L be non empty ZeroStr ; ::_thesis: for a, b being Element of L holds
( a | (X,L) = b | (X,L) iff a = b )
let a, b be Element of L; ::_thesis: ( a | (X,L) = b | (X,L) iff a = b )
set m = (0_ (X,L)) +* ((EmptyBag X),a);
reconsider m = (0_ (X,L)) +* ((EmptyBag X),a) as Function of (Bags X), the carrier of L ;
reconsider m = m as Function of (Bags X),L ;
reconsider m = m as Series of X,L ;
set k = (0_ (X,L)) +* ((EmptyBag X),b);
reconsider k = (0_ (X,L)) +* ((EmptyBag X),b) as Function of (Bags X), the carrier of L ;
reconsider k = k as Function of (Bags X),L ;
reconsider k = k as Series of X,L ;
 dom ((EmptyBag X) .--> a) = {(EmptyBag X)} by FUNCOP_1:13;
then A1: EmptyBag X in dom ((EmptyBag X) .--> a) by TARSKI:def_1;
 dom ((EmptyBag X) .--> b) = {(EmptyBag X)} by FUNCOP_1:13;
then A2: EmptyBag X in dom ((EmptyBag X) .--> b) by TARSKI:def_1;
dom (0_ (X,L)) = dom ((Bags X) --> (0. L)) by POLYNOM1:def_7
.= Bags X by FUNCOP_1:13 ;
then A3: k . (EmptyBag X) = ((0_ (X,L)) +* ((EmptyBag X) .--> b)) . (EmptyBag X) by FUNCT_7:def_3
.= ((EmptyBag X) .--> b) . (EmptyBag X) by A2, FUNCT_4:13
.= b by FUNCOP_1:72 ;
dom (0_ (X,L)) = dom ((Bags X) --> (0. L)) by POLYNOM1:def_7
.= Bags X by FUNCOP_1:13 ;
then m . (EmptyBag X) = ((0_ (X,L)) +* ((EmptyBag X) .--> a)) . (EmptyBag X) by FUNCT_7:def_3
.= ((EmptyBag X) .--> a) . (EmptyBag X) by A1, FUNCT_4:13
.= a by FUNCOP_1:72 ;
hence  ( a | (X,L) = b | (X,L) iff a = b ) by A3; ::_thesis: verum
end;

theorem :: POLYNOM7:22
for X being set
for L being non empty ZeroStr
for a being Element of L holds
( Support (a | (X,L)) = {} or Support (a | (X,L)) = {(EmptyBag X)} ) by Th15;

theorem Th23: :: POLYNOM7:23
for X being set
for L being non empty ZeroStr
for a being Element of L holds
( term (a | (X,L)) = EmptyBag X & coefficient (a | (X,L)) = a )
proof
let X be set ; ::_thesis: for L being non empty ZeroStr
for a being Element of L holds
( term (a | (X,L)) = EmptyBag X & coefficient (a | (X,L)) = a )
let L be non empty ZeroStr ; ::_thesis: for a being Element of L holds
( term (a | (X,L)) = EmptyBag X & coefficient (a | (X,L)) = a )
let a be Element of L; ::_thesis: ( term (a | (X,L)) = EmptyBag X & coefficient (a | (X,L)) = a )
set m = (0_ (X,L)) +* ((EmptyBag X),a);
reconsider m = (0_ (X,L)) +* ((EmptyBag X),a) as Function of (Bags X), the carrier of L ;
reconsider m = m as Function of (Bags X),L ;
reconsider m = m as Series of X,L ;
 dom ((EmptyBag X) .--> a) = {(EmptyBag X)} by FUNCOP_1:13;
then A1: EmptyBag X in dom ((EmptyBag X) .--> a) by TARSKI:def_1;
dom (0_ (X,L)) = dom ((Bags X) --> (0. L)) by POLYNOM1:def_7
.= Bags X by FUNCOP_1:13 ;
then m . (EmptyBag X) = ((0_ (X,L)) +* ((EmptyBag X) .--> a)) . (EmptyBag X) by FUNCT_7:def_3
.= ((EmptyBag X) .--> a) . (EmptyBag X) by A1, FUNCT_4:13
.= a by FUNCOP_1:72 ;
hence  ( term (a | (X,L)) = EmptyBag X & coefficient (a | (X,L)) = a ) by Lm2; ::_thesis: verum
end;

theorem Th24: :: POLYNOM7:24
for n being Ordinal
for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for c being ConstPoly of n,L
for x being Function of n,L holds eval (c,x) = coefficient c
proof
let n be Ordinal; ::_thesis: for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for c being ConstPoly of n,L
for x being Function of n,L holds eval (c,x) = coefficient c
let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; ::_thesis: for c being ConstPoly of n,L
for x being Function of n,L holds eval (c,x) = coefficient c
let c be ConstPoly of n,L; ::_thesis: for x being Function of n,L holds eval (c,x) = coefficient c
let x be Function of n,L; ::_thesis: eval (c,x) = coefficient c
consider y being FinSequence of the carrier of L such that
A1: len y = len (SgmX ((BagOrder n),(Support c))) and
A2: eval (c,x) = Sum y and
A3: for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((c * (SgmX ((BagOrder n),(Support c)))) /. i) * (eval ((((SgmX ((BagOrder n),(Support c))) /. i) @),x)) by POLYNOM2:def_4;
now__::_thesis:_(_(_coefficient_c_=_0._L_&_eval_(c,x)_=_coefficient_c_)_or_(_coefficient_c_<>_0._L_&_eval_(c,x)_=_coefficient_c_)_)
percases ( coefficient c = 0. L or coefficient c <> 0. L ) ;
caseA4: coefficient c = 0. L ; ::_thesis: eval (c,x) = coefficient c
 Support c = {}
proof
set u = the Element of Support c;
assume A5: Support c <> {} ; ::_thesis: contradiction
then  the Element of Support c in Support c ;
then reconsider u = the Element of Support c as Element of Bags n ;
 c . u <> 0. L by A5, POLYNOM1:def_3;
then  u <> EmptyBag n by A4, Lm2;
then  c . u = 0. L by Def7;
hence  contradiction by A5, POLYNOM1:def_3; ::_thesis: verum
end;
then reconsider Sc = Support c as empty Subset of (Bags n) ;
 SgmX ((BagOrder n),Sc) = {} by POLYNOM2:7, POLYNOM2:18;
then  y = <*> the carrier of L by A1;
hence  eval (c,x) = coefficient c by A2, A4, RLVECT_1:43; ::_thesis: verum
end;
caseA6: coefficient c <> 0. L ; ::_thesis: eval (c,x) = coefficient c
reconsider sc = Support c as finite Subset of (Bags n) ;
set sg = SgmX ((BagOrder n),sc);
A7: BagOrder n linearly_orders sc by POLYNOM2:18;
A8: for u being set st u in Support c holds
u in {(EmptyBag n)}
proof
let u be set ; ::_thesis: ( u in Support c implies u in {(EmptyBag n)} )
assume A9: u in Support c ; ::_thesis: u in {(EmptyBag n)}
assume A10: not u in {(EmptyBag n)} ; ::_thesis: contradiction
reconsider u = u as Element of Bags n by A9;
 u <> EmptyBag n by A10, TARSKI:def_1;
then  c . u = 0. L by Def7;
hence  contradiction by A9, POLYNOM1:def_3; ::_thesis: verum
end;
 for u being set st u in {(EmptyBag n)} holds
u in Support c
proof
let u be set ; ::_thesis: ( u in {(EmptyBag n)} implies u in Support c )
assume A11: u in {(EmptyBag n)} ; ::_thesis: u in Support c
then A12: u = EmptyBag n by TARSKI:def_1;
reconsider u = u as Element of Bags n by A11;
 c . u <> 0. L by A6, A12, Lm2;
hence  u in Support c by POLYNOM1:def_3; ::_thesis: verum
end;
then  Support c = {(EmptyBag n)} by A8, TARSKI:1;
then A13: rng (SgmX ((BagOrder n),sc)) = {(EmptyBag n)} by A7, PRE_POLY:def_2;
then A14: EmptyBag n in rng (SgmX ((BagOrder n),sc)) by TARSKI:def_1;
then A15: 1 in dom (SgmX ((BagOrder n),sc)) by FINSEQ_3:31;
then A16: (SgmX ((BagOrder n),sc)) . 1 in rng (SgmX ((BagOrder n),sc)) by FUNCT_1:3;
A17: for u being set st u in dom (SgmX ((BagOrder n),sc)) holds
u in {1}
proof
let u be set ; ::_thesis: ( u in dom (SgmX ((BagOrder n),sc)) implies u in {1} )
assume A18: u in dom (SgmX ((BagOrder n),sc)) ; ::_thesis: u in {1}
assume A19: not u in {1} ; ::_thesis: contradiction
reconsider u = u as Element of NAT by A18;
 (SgmX ((BagOrder n),sc)) /. u = (SgmX ((BagOrder n),sc)) . u by A18, PARTFUN1:def_6;
then A20: (SgmX ((BagOrder n),sc)) /. u in rng (SgmX ((BagOrder n),sc)) by A18, FUNCT_1:3;
A21: u <> 1 by A19, TARSKI:def_1;
A22: 1 < u
proof
consider k being Nat such that
A23: dom (SgmX ((BagOrder n),sc)) = Seg k by FINSEQ_1:def_2;
 Seg k =  {  m where m is Element of NAT : ( 1 <= m & m <= k )  }  by FINSEQ_1:def_1;
then  ex m9 being Element of NAT st
( m9 = u & 1 <= m9 & m9 <= k ) by A18, A23;
hence  1 < u by A21, XXREAL_0:1; ::_thesis: verum
end;
 (SgmX ((BagOrder n),sc)) /. 1 = (SgmX ((BagOrder n),sc)) . 1 by A14, A18, FINSEQ_3:31, PARTFUN1:def_6;
then  (SgmX ((BagOrder n),sc)) /. 1 in rng (SgmX ((BagOrder n),sc)) by A15, FUNCT_1:3;
then (SgmX ((BagOrder n),sc)) /. 1 = EmptyBag n by A13, TARSKI:def_1
.= (SgmX ((BagOrder n),sc)) /. u by A13, A20, TARSKI:def_1 ;
hence  contradiction by A7, A15, A18, A22, PRE_POLY:def_2; ::_thesis: verum
end;
 for u being set st u in {1} holds
u in dom (SgmX ((BagOrder n),sc)) by A15, TARSKI:def_1;
then A24: dom (SgmX ((BagOrder n),sc)) = Seg 1 by A17, FINSEQ_1:2, TARSKI:1;
then A25: 1 in dom (SgmX ((BagOrder n),sc)) by FINSEQ_1:2, TARSKI:def_1;
 (SgmX ((BagOrder n),sc)) /. 1 = (SgmX ((BagOrder n),sc)) . 1 by A15, PARTFUN1:def_6;
then  (SgmX ((BagOrder n),sc)) /. 1 in rng (SgmX ((BagOrder n),sc)) by A25, FUNCT_1:3;
then A26: (SgmX ((BagOrder n),sc)) /. 1 = EmptyBag n by A13, TARSKI:def_1;
A27: len (SgmX ((BagOrder n),sc)) = 1 by A24, FINSEQ_1:def_3;
 dom c = Bags n by FUNCT_2:def_1;
then  1 in dom (c * (SgmX ((BagOrder n),sc))) by A13, A15, A16, FUNCT_1:11;
then A28: (c * (SgmX ((BagOrder n),sc))) /. 1 = (c * (SgmX ((BagOrder n),sc))) . 1 by PARTFUN1:def_6
.= c . ((SgmX ((BagOrder n),sc)) . 1) by A15, FUNCT_1:13
.= c . (EmptyBag n) by A13, A16, TARSKI:def_1
.= coefficient c by Lm2 ;
dom y = Seg (len y) by FINSEQ_1:def_3
.= dom (SgmX ((BagOrder n),sc)) by A1, FINSEQ_1:def_3 ;
then y . 1 = y /. 1 by A25, PARTFUN1:def_6
.= ((c * (SgmX ((BagOrder n),sc))) /. 1) * (eval ((((SgmX ((BagOrder n),sc)) /. 1) @),x)) by A1, A3, A27
.= (coefficient c) * (eval ((EmptyBag n),x)) by A26, A28, POLYNOM2:def_3
.= (coefficient c) * (1. L) by POLYNOM2:14
.= coefficient c by VECTSP_1:def_6 ;
then  y = <*(coefficient c)*> by A1, A27, FINSEQ_1:40;
hence  eval (c,x) = coefficient c by A2, RLVECT_1:44; ::_thesis: verum
end;
end;
end;
hence  eval (c,x) = coefficient c ; ::_thesis: verum
end;

theorem Th25: :: POLYNOM7:25
for n being Ordinal
for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for a being Element of L
for x being Function of n,L holds eval ((a | (n,L)),x) = a
proof
let n be Ordinal; ::_thesis: for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for a being Element of L
for x being Function of n,L holds eval ((a | (n,L)),x) = a
let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; ::_thesis: for a being Element of L
for x being Function of n,L holds eval ((a | (n,L)),x) = a
let a be Element of L; ::_thesis: for x being Function of n,L holds eval ((a | (n,L)),x) = a
let x be Function of n,L; ::_thesis: eval ((a | (n,L)),x) = a
thus  eval ((a | (n,L)),x) = coefficient (a | (n,L)) by Th24
.= a by Th23 ; ::_thesis: verum
end;

begin

definition
let X be set ;
let L be non empty multLoopStr_0 ;
let p be Series of X,L;
let a be Element of L;
funca * p ->  Series of X,L means :Def9: :: POLYNOM7:def 9
 for b being bag of X holds it . b = a * (p . b);
existence
 ex b1 being Series of X,L st
for b being bag of X holds b1 . b = a * (p . b)
proof
deffunc H1( Element of Bags X) ->  Element of the carrier of L = a * (p . $1);
consider f being Function of (Bags X), the carrier of L such that
A1: for x being Element of Bags X holds f . x = H1(x) from FUNCT_2:sch_4();
reconsider f = f as Function of (Bags X),L ;
reconsider f = f as Series of X,L ;
reconsider f = f as Series of X,L ;
take  f ; ::_thesis: for b being bag of X holds f . b = a * (p . b)
let x be bag of X; ::_thesis: f . x = a * (p . x)
 x in Bags X by PRE_POLY:def_12;
hence  f . x = a * (p . x) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Series of X,L st ( for b being bag of X holds b1 . b = a * (p . b) ) & ( for b being bag of X holds b2 . b = a * (p . b) ) holds
b1 = b2
proof
let p1, p2 be Series of X,L; ::_thesis: ( ( for b being bag of X holds p1 . b = a * (p . b) ) & ( for b being bag of X holds p2 . b = a * (p . b) ) implies p1 = p2 )
assume that
A2: for b being bag of X holds p1 . b = a * (p . b) and
A3: for b being bag of X holds p2 . b = a * (p . b) ; ::_thesis: p1 = p2
now__::_thesis:_for_b_being_Element_of_Bags_X_holds_p1_._b_=_p2_._b
let b be Element of Bags X; ::_thesis: p1 . b = p2 . b
reconsider b9 = b as bag of X ;
thus p1 . b = a * (p . b9) by A2
.= p2 . b by A3 ; ::_thesis: verum
end;
hence  p1 = p2 by FUNCT_2:63; ::_thesis: verum
end;
funcp * a ->  Series of X,L means :Def10: :: POLYNOM7:def 10
 for b being bag of X holds it . b = (p . b) * a;
existence
 ex b1 being Series of X,L st
for b being bag of X holds b1 . b = (p . b) * a
proof
deffunc H1( Element of Bags X) ->  Element of the carrier of L = (p . $1) * a;
consider f being Function of (Bags X), the carrier of L such that
A4: for x being Element of Bags X holds f . x = H1(x) from FUNCT_2:sch_4();
reconsider f = f as Function of (Bags X),L ;
reconsider f = f as Series of X,L ;
reconsider f = f as Series of X,L ;
take  f ; ::_thesis: for b being bag of X holds f . b = (p . b) * a
let x be bag of X; ::_thesis: f . x = (p . x) * a
 x in Bags X by PRE_POLY:def_12;
hence  f . x = (p . x) * a by A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Series of X,L st ( for b being bag of X holds b1 . b = (p . b) * a ) & ( for b being bag of X holds b2 . b = (p . b) * a ) holds
b1 = b2
proof
let p1, p2 be Series of X,L; ::_thesis: ( ( for b being bag of X holds p1 . b = (p . b) * a ) & ( for b being bag of X holds p2 . b = (p . b) * a ) implies p1 = p2 )
assume that
A5: for b being bag of X holds p1 . b = (p . b) * a and
A6: for b being bag of X holds p2 . b = (p . b) * a ; ::_thesis: p1 = p2
now__::_thesis:_for_b_being_Element_of_Bags_X_holds_p1_._b_=_p2_._b
let b be Element of Bags X; ::_thesis: p1 . b = p2 . b
reconsider b9 = b as bag of X ;
thus p1 . b = (p . b9) * a by A5
.= p2 . b by A6 ; ::_thesis: verum
end;
hence  p1 = p2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines * POLYNOM7:def_9_:_
 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 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 = p * a iff for b being bag of X holds b5 . b = (p . b) * a );

registration
let X be set ;
let L be non empty add-cancelable right_zeroed distributive left_zeroed doubleLoopStr ;
let p be finite-Support Series of X,L;
let a be Element of L;
clustera * p ->  finite-Support ;
coherence
 a * p is finite-Support
proof
set ap = a * p;
now__::_thesis:_for_u_being_set_st_u_in_Support_(a_*_p)_holds_
u_in_Support_p
let u be set ; ::_thesis: ( u in Support (a * p) implies u in Support p )
assume A1: u in Support (a * p) ; ::_thesis: u in Support p
then reconsider u9 = u as Element of Bags X ;
 (a * p) . u <> 0. L by A1, POLYNOM1:def_3;
then  a * (p . u9) <> 0. L by Def9;
then  p . u9 <> 0. L by BINOM:2;
hence  u in Support p by POLYNOM1:def_3; ::_thesis: verum
end;
then  ( Support p is finite & Support (a * p) c= Support p ) by POLYNOM1:def_4, TARSKI:def_3;
hence  a * p is finite-Support by POLYNOM1:def_4; ::_thesis: verum
end;
clusterp * a ->  finite-Support ;
coherence
 p * a is finite-Support
proof
set ap = p * a;
now__::_thesis:_for_u_being_set_st_u_in_Support_(p_*_a)_holds_
u_in_Support_p
let u be set ; ::_thesis: ( u in Support (p * a) implies u in Support p )
assume A2: u in Support (p * a) ; ::_thesis: u in Support p
then reconsider u9 = u as Element of Bags X ;
 (p * a) . u <> 0. L by A2, POLYNOM1:def_3;
then  (p . u9) * a <> 0. L by Def10;
then  p . u9 <> 0. L by BINOM:1;
hence  u in Support p by POLYNOM1:def_3; ::_thesis: verum
end;
then  ( Support p is finite & Support (p * a) c= Support p ) by POLYNOM1:def_4, TARSKI:def_3;
hence  p * a is finite-Support by POLYNOM1:def_4; ::_thesis: verum
end;
end;

theorem :: POLYNOM7:26
for X being set
for L being non empty commutative multLoopStr_0
for p being Series of X,L
for a being Element of L holds a * p = p * a
proof
let n be set ; ::_thesis: for L being non empty commutative multLoopStr_0
for p being Series of n,L
for a being Element of L holds a * p = p * a
let L be non empty commutative multLoopStr_0 ; ::_thesis: for p being Series of n,L
for a being Element of L holds a * p = p * a
let p be Series of n,L; ::_thesis: for a being Element of L holds a * p = p * a
let a be Element of L; ::_thesis: a * p = p * a
now__::_thesis:_for_b_being_Element_of_Bags_n_holds_(a_*_p)_._b_=_(p_*_a)_._b
let b be Element of Bags n; ::_thesis: (a * p) . b = (p * a) . b
reconsider b9 = b as bag of n ;
thus (a * p) . b = a * (p . b9) by Def9
.= (p * a) . b by Def10 ; ::_thesis: verum
end;
hence  a * p = p * a by FUNCT_2:63; ::_thesis: verum
end;

theorem Th27: :: POLYNOM7:27
for n being Ordinal
for L being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr
for p being Series of n,L
for a being Element of L holds a * p = (a | (n,L)) *' p
proof
let n be Ordinal; ::_thesis: for L being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr
for p being Series of n,L
for a being Element of L holds a * p = (a | (n,L)) *' p
let L be non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr ; ::_thesis: for p being Series of n,L
for a being Element of L holds a * p = (a | (n,L)) *' p
let p be Series of n,L; ::_thesis: for a being Element of L holds a * p = (a | (n,L)) *' p
let a be Element of L; ::_thesis: a * p = (a | (n,L)) *' p
A1: for x being set st x in Bags n holds
(a * p) . x = ((a | (n,L)) *' p) . x
proof
set O = a | (n,L);
set cL = the carrier of L;
let x be set ; ::_thesis: ( x in Bags n implies (a * p) . x = ((a | (n,L)) *' p) . x )
assume  x in Bags n ; ::_thesis: (a * p) . x = ((a | (n,L)) *' p) . x
then reconsider b = x as bag of n ;
A2: for b being Element of Bags n holds ((a | (n,L)) *' p) . b = a * (p . b)
proof
let b be Element of Bags n; ::_thesis: ((a | (n,L)) *' p) . b = a * (p . b)
consider s being FinSequence of the carrier of L such that
A3: ((a | (n,L)) *' p) . b = Sum s and
A4: len s = len (decomp b) and
A5: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = ((a | (n,L)) . b1) * (p . b2) ) by POLYNOM1:def_9;
 not s is empty by A4;
then consider s1 being Element of the carrier of L, t being FinSequence of the carrier of L such that
A6: s1 = s . 1 and
A7: s = <*s1*> ^ t by FINSEQ_3:102;
A8: Sum s = (Sum <*s1*>) + (Sum t) by A7, RLVECT_1:41;
A9: now__::_thesis:_Sum_t_=_0._L
percases ( t = <*> the carrier of L or t <> <*> the carrier of L ) ;
suppose t = <*> the carrier of L ; ::_thesis: Sum t = 0. L
hence  Sum t = 0. L by RLVECT_1:43; ::_thesis: verum
end;
supposeA10: t <> <*> the carrier of L ; ::_thesis: Sum t = 0. L
now__::_thesis:_for_k_being_Nat_st_k_in_dom_t_holds_
t_/._k_=_0._L
let k be Nat; ::_thesis: ( k in dom t implies t /. b1 = 0. L )
A11: len s = (len t) + (len <*s1*>) by A7, FINSEQ_1:22
.= (len t) + 1 by FINSEQ_1:39 ;
assume A12: k in dom t ; ::_thesis: t /. b1 = 0. L
then A13: t /. k = t . k by PARTFUN1:def_6
.= s . (k + 1) by A7, A12, FINSEQ_3:103 ;
 1 <= k by A12, FINSEQ_3:25;
then A14: 1 < k + 1 by NAT_1:13;
 k <= len t by A12, FINSEQ_3:25;
then A15: k + 1 <= len s by A11, XREAL_1:6;
then A16: k + 1 in dom (decomp b) by A4, A14, FINSEQ_3:25;
A17: dom s = dom (decomp b) by A4, FINSEQ_3:29;
then A18: s /. (k + 1) = s . (k + 1) by A16, PARTFUN1:def_6;
percases ( k + 1 < len s or k + 1 = len s ) by A15, XXREAL_0:1;
supposeA19: k + 1 < len s ; ::_thesis: t /. b1 = 0. L
reconsider k1 = k as Element of NAT by ORDINAL1:def_12;
consider b1, b2 being bag of n such that
A20: (decomp b) /. (k1 + 1) = <*b1,b2*> and
A21: s /. (k1 + 1) = ((a | (n,L)) . b1) * (p . b2) by A5, A17, A16;
 b1 <> EmptyBag n by A4, A14, A19, A20, PRE_POLY:72;
hence t /. k = (0. L) * (p . b2) by A13, A18, A21, Th18
.= 0. L by VECTSP_1:7 ;
::_thesis: verum
end;
supposeA22: k + 1 = len s ; ::_thesis: t /. b1 = 0. L
A23: now__::_thesis:_not_b_=_EmptyBag_n
assume  b = EmptyBag n ; ::_thesis: contradiction
then  decomp b = <*<*(EmptyBag n),(EmptyBag n)*>*> by PRE_POLY:73;
then  (len t) + 1 = 0 + 1 by A4, A11, FINSEQ_1:39;
hence  contradiction by A10; ::_thesis: verum
end;
consider b1, b2 being bag of n such that
A24: (decomp b) /. (k + 1) = <*b1,b2*> and
A25: s /. (k + 1) = ((a | (n,L)) . b1) * (p . b2) by A5, A17, A16;
 (decomp b) /. (len s) = <*b,(EmptyBag n)*> by A4, PRE_POLY:71;
then  ( b2 = EmptyBag n & b1 = b ) by A22, A24, FINSEQ_1:77;
then s . (k + 1) = (0. L) * (p . (EmptyBag n)) by A18, A25, A23, Th18
.= 0. L by VECTSP_1:7 ;
hence  t /. k = 0. L by A13; ::_thesis: verum
end;
end;
end;
hence  Sum t = 0. L by MATRLIN:11; ::_thesis: verum
end;
end;
end;
A26: not s is empty by A4;
then consider b1, b2 being bag of n such that
A27: (decomp b) /. 1 = <*b1,b2*> and
A28: s /. 1 = ((a | (n,L)) . b1) * (p . b2) by A5, FINSEQ_5:6;
 1 in dom s by A26, FINSEQ_5:6;
then A29: s /. 1 = s . 1 by PARTFUN1:def_6;
 (decomp b) /. 1 = <*(EmptyBag n),b*> by PRE_POLY:71;
then A30: ( b2 = b & b1 = EmptyBag n ) by A27, FINSEQ_1:77;
Sum <*s1*> = s1 by RLVECT_1:44
.= a * (p . b) by A6, A28, A30, A29, Th18 ;
hence  ((a | (n,L)) *' p) . b = a * (p . b) by A3, A8, A9, RLVECT_1:4; ::_thesis: verum
end;
 b is Element of Bags n by PRE_POLY:def_12;
then ((a | (n,L)) *' p) . b = a * (p . b) by A2
.= (a * p) . b by Def9 ;
hence  (a * p) . x = ((a | (n,L)) *' p) . x ; ::_thesis: verum
end;
 ( Bags n = dom (a * p) & Bags n = dom ((a | (n,L)) *' p) ) by FUNCT_2:def_1;
hence  a * p = (a | (n,L)) *' p by A1, FUNCT_1:2; ::_thesis: verum
end;

theorem Th28: :: POLYNOM7:28
for n being Ordinal
for L being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for p being Series of n,L
for a being Element of L holds p * a = p *' (a | (n,L))
proof
let n be Ordinal; ::_thesis: for L being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for p being Series of n,L
for a being Element of L holds p * a = p *' (a | (n,L))
let L be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ; ::_thesis: for p being Series of n,L
for a being Element of L holds p * a = p *' (a | (n,L))
let p be Series of n,L; ::_thesis: for a being Element of L holds p * a = p *' (a | (n,L))
let a be Element of L; ::_thesis: p * a = p *' (a | (n,L))
A1: for x being set st x in Bags n holds
(p * a) . x = (p *' (a | (n,L))) . x
proof
set O = a | (n,L);
set cL = the carrier of L;
let x be set ; ::_thesis: ( x in Bags n implies (p * a) . x = (p *' (a | (n,L))) . x )
assume  x in Bags n ; ::_thesis: (p * a) . x = (p *' (a | (n,L))) . x
then reconsider b = x as bag of n ;
A2: for b being Element of Bags n holds (p *' (a | (n,L))) . b = (p . b) * a
proof
let b be Element of Bags n; ::_thesis: (p *' (a | (n,L))) . b = (p . b) * a
consider s being FinSequence of the carrier of L such that
A3: (p *' (a | (n,L))) . b = Sum s and
A4: len s = len (decomp b) and
A5: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * ((a | (n,L)) . b2) ) by POLYNOM1:def_9;
consider t being FinSequence of the carrier of L, s1 being Element of the carrier of L such that
A6: s = t ^ <*s1*> by A4, FINSEQ_2:19;
A7: now__::_thesis:_Sum_t_=_0._L
percases ( t = <*> the carrier of L or t <> <*> the carrier of L ) ;
suppose t = <*> the carrier of L ; ::_thesis: Sum t = 0. L
hence  Sum t = 0. L by RLVECT_1:43; ::_thesis: verum
end;
supposeA8: t <> <*> the carrier of L ; ::_thesis: Sum t = 0. L
now__::_thesis:_for_k_being_Nat_st_k_in_dom_t_holds_
t_/._k_=_0._L
let k be Nat; ::_thesis: ( k in dom t implies t /. b1 = 0. L )
A9: len s = (len t) + (len <*s1*>) by A6, FINSEQ_1:22
.= (len t) + 1 by FINSEQ_1:39 ;
assume A10: k in dom t ; ::_thesis: t /. b1 = 0. L
then A11: t /. k = t . k by PARTFUN1:def_6
.= s . k by A6, A10, FINSEQ_1:def_7 ;
 k <= len t by A10, FINSEQ_3:25;
then A12: k < len s by A9, NAT_1:13;
A13: 1 <= k by A10, FINSEQ_3:25;
then A14: k in dom (decomp b) by A4, A12, FINSEQ_3:25;
A15: dom s = dom (decomp b) by A4, FINSEQ_3:29;
then A16: s /. k = s . k by A14, PARTFUN1:def_6;
percases ( 1 < k or k = 1 ) by A13, XXREAL_0:1;
supposeA17: 1 < k ; ::_thesis: t /. b1 = 0. L
reconsider k1 = k as Element of NAT by ORDINAL1:def_12;
consider b1, b2 being bag of n such that
A18: (decomp b) /. k1 = <*b1,b2*> and
A19: s /. k1 = (p . b1) * ((a | (n,L)) . b2) by A5, A15, A14;
 b2 <> EmptyBag n by A4, A12, A17, A18, PRE_POLY:72;
hence t /. k = (p . b1) * (0. L) by A11, A16, A19, Th18
.= 0. L by VECTSP_1:6 ;
::_thesis: verum
end;
supposeA20: k = 1 ; ::_thesis: t /. b1 = 0. L
A21: now__::_thesis:_not_b_=_EmptyBag_n
assume  b = EmptyBag n ; ::_thesis: contradiction
then  decomp b = <*<*(EmptyBag n),(EmptyBag n)*>*> by PRE_POLY:73;
then  (len t) + 1 = 0 + 1 by A4, A9, FINSEQ_1:39;
hence  contradiction by A8; ::_thesis: verum
end;
consider b1, b2 being bag of n such that
A22: (decomp b) /. k = <*b1,b2*> and
A23: s /. k = (p . b1) * ((a | (n,L)) . b2) by A5, A15, A14;
 (decomp b) /. 1 = <*(EmptyBag n),b*> by PRE_POLY:71;
then  ( b1 = EmptyBag n & b2 = b ) by A20, A22, FINSEQ_1:77;
then s . k = (p . (EmptyBag n)) * (0. L) by A16, A23, A21, Th18
.= 0. L by VECTSP_1:6 ;
hence  t /. k = 0. L by A11; ::_thesis: verum
end;
end;
end;
hence  Sum t = 0. L by MATRLIN:11; ::_thesis: verum
end;
end;
end;
A24: s . (len s) = (t ^ <*s1*>) . ((len t) + 1) by A6, FINSEQ_2:16
.= s1 by FINSEQ_1:42 ;
A25: Sum s = (Sum t) + (Sum <*s1*>) by A6, RLVECT_1:41;
 not s is empty by A4;
then A26: len s in dom s by FINSEQ_5:6;
then consider b1, b2 being bag of n such that
A27: (decomp b) /. (len s) = <*b1,b2*> and
A28: s /. (len s) = (p . b1) * ((a | (n,L)) . b2) by A5;
A29: s /. (len s) = s . (len s) by A26, PARTFUN1:def_6;
 (decomp b) /. (len s) = <*b,(EmptyBag n)*> by A4, PRE_POLY:71;
then A30: ( b1 = b & b2 = EmptyBag n ) by A27, FINSEQ_1:77;
Sum <*s1*> = s1 by RLVECT_1:44
.= (p . b) * a by A28, A30, A29, A24, Th18 ;
hence  (p *' (a | (n,L))) . b = (p . b) * a by A3, A25, A7, RLVECT_1:4; ::_thesis: verum
end;
 b is Element of Bags n by PRE_POLY:def_12;
then (p *' (a | (n,L))) . b = (p . b) * a by A2
.= (p * a) . b by Def10 ;
hence  (p * a) . x = (p *' (a | (n,L))) . x ; ::_thesis: verum
end;
 ( Bags n = dom (p * a) & Bags n = dom (p *' (a | (n,L))) ) by FUNCT_2:def_1;
hence  p * a = p *' (a | (n,L)) by A1, FUNCT_1:2; ::_thesis: verum
end;

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))
proof
let n be Ordinal; ::_thesis: 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))
let L be non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive left_zeroed doubleLoopStr ; ::_thesis: 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))
let p be Polynomial of n,L; ::_thesis: for a being Element of L
for x being Function of n,L holds eval (((a | (n,L)) *' p),x) = a * (eval (p,x))
let a be Element of L; ::_thesis: for x being Function of n,L holds eval (((a | (n,L)) *' p),x) = a * (eval (p,x))
let x be Function of n,L; ::_thesis: eval (((a | (n,L)) *' p),x) = a * (eval (p,x))
thus  eval (((a | (n,L)) *' p),x) = (eval ((a | (n,L)),x)) * (eval (p,x)) by POLYNOM2:25
.= a * (eval (p,x)) by Th25 ; ::_thesis: verum
end;

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
proof
let n be Ordinal; ::_thesis: 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
let L be non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive left_zeroed doubleLoopStr ; ::_thesis: 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
let p be Polynomial of n,L; ::_thesis: for a being Element of L
for x being Function of n,L holds eval ((p *' (a | (n,L))),x) = (eval (p,x)) * a
let a be Element of L; ::_thesis: for x being Function of n,L holds eval ((p *' (a | (n,L))),x) = (eval (p,x)) * a
let x be Function of n,L; ::_thesis: eval ((p *' (a | (n,L))),x) = (eval (p,x)) * a
thus  eval ((p *' (a | (n,L))),x) = (eval (p,x)) * (eval ((a | (n,L)),x)) by POLYNOM2:25
.= (eval (p,x)) * a by Th25 ; ::_thesis: verum
end;

theorem :: POLYNOM7:29
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 * p),x) = a * (eval (p,x))
proof
let n be Ordinal; ::_thesis: 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 * p),x) = a * (eval (p,x))
let L be non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive left_zeroed doubleLoopStr ; ::_thesis: for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval ((a * p),x) = a * (eval (p,x))
let p be Polynomial of n,L; ::_thesis: for a being Element of L
for x being Function of n,L holds eval ((a * p),x) = a * (eval (p,x))
let a be Element of L; ::_thesis: for x being Function of n,L holds eval ((a * p),x) = a * (eval (p,x))
let x be Function of n,L; ::_thesis: eval ((a * p),x) = a * (eval (p,x))
thus  eval ((a * p),x) = eval (((a | (n,L)) *' p),x) by Th27
.= a * (eval (p,x)) by Lm4 ; ::_thesis: verum
end;

theorem :: POLYNOM7:30
for n being Ordinal
for L being non trivial left_add-cancelable right_complementable add-associative right_zeroed associative well-unital distributive domRing-like 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 * p),x) = a * (eval (p,x))
proof
let n be Ordinal; ::_thesis: for L being non trivial left_add-cancelable right_complementable add-associative right_zeroed associative well-unital distributive domRing-like 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 * p),x) = a * (eval (p,x))
let L be non trivial left_add-cancelable right_complementable add-associative right_zeroed associative well-unital distributive domRing-like left_zeroed doubleLoopStr ; ::_thesis: for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval ((a * p),x) = a * (eval (p,x))
let p be Polynomial of n,L; ::_thesis: for a being Element of L
for x being Function of n,L holds eval ((a * p),x) = a * (eval (p,x))
let a be Element of L; ::_thesis: for x being Function of n,L holds eval ((a * p),x) = a * (eval (p,x))
let x be Function of n,L; ::_thesis: eval ((a * p),x) = a * (eval (p,x))
consider y being FinSequence of the carrier of L such that
A1: len y = len (SgmX ((BagOrder n),(Support (a * p)))) and
A2: eval ((a * p),x) = Sum y and
A3: for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = (((a * p) * (SgmX ((BagOrder n),(Support (a * p))))) /. i) * (eval ((((SgmX ((BagOrder n),(Support (a * p)))) /. i) @),x)) by POLYNOM2:def_4;
A4: BagOrder n linearly_orders Support (a * p) by POLYNOM2:18;
consider z being FinSequence of the carrier of L such that
A5: len z = len (SgmX ((BagOrder n),(Support p))) and
A6: eval (p,x) = Sum z and
A7: for i being Element of NAT st 1 <= i & i <= len z holds
z /. i = ((p * (SgmX ((BagOrder n),(Support p)))) /. i) * (eval ((((SgmX ((BagOrder n),(Support p))) /. i) @),x)) by POLYNOM2:def_4;
percases ( a = 0. L or a <> 0. L ) ;
supposeA8: a = 0. L ; ::_thesis: eval ((a * p),x) = a * (eval (p,x))
A9: now__::_thesis:_for_b_being_bag_of_n_holds_(a_*_p)_._b_=_0._L
let b be bag of n; ::_thesis: (a * p) . b = 0. L
thus (a * p) . b = a * (p . b) by Def9
.= 0. L by A8, BINOM:1 ; ::_thesis: verum
end;
now__::_thesis:_not_Support_(a_*_p)_<>_{}
assume  Support (a * p) <> {} ; ::_thesis: contradiction
then reconsider sp = Support (a * p) as non empty Subset of (Bags n) ;
set c = the Element of sp;
 (a * p) . the Element of sp <> 0. L by POLYNOM1:def_3;
hence  contradiction by A9; ::_thesis: verum
end;
then  rng (SgmX ((BagOrder n),(Support (a * p)))) = {} by A4, PRE_POLY:def_2;
then  SgmX ((BagOrder n),(Support (a * p))) = {} by RELAT_1:41;
then  y = <*> the carrier of L by A1;
then  Sum y = 0. L by RLVECT_1:43
.= a * (Sum z) by A8, BINOM:1 ;
hence  eval ((a * p),x) = a * (eval (p,x)) by A2, A6; ::_thesis: verum
end;
supposeA10: a <> 0. L ; ::_thesis: eval ((a * p),x) = a * (eval (p,x))
A11: for u being set st u in Support (a * p) holds
u in Support p
proof
let u be set ; ::_thesis: ( u in Support (a * p) implies u in Support p )
assume A12: u in Support (a * p) ; ::_thesis: u in Support p
then reconsider u9 = u as Element of Bags n ;
 (a * p) . u <> 0. L by A12, POLYNOM1:def_3;
then  a * (p . u9) <> 0. L by Def9;
then  p . u9 <> 0. L by BINOM:2;
hence  u in Support p by POLYNOM1:def_3; ::_thesis: verum
end;
A13: for u being set st u in Support p holds
u in Support (a * p)
proof
let u be set ; ::_thesis: ( u in Support p implies u in Support (a * p) )
assume A14: u in Support p ; ::_thesis: u in Support (a * p)
then reconsider u9 = u as Element of Bags n ;
 p . u <> 0. L by A14, POLYNOM1:def_3;
then  a * (p . u9) <> 0. L by A10, VECTSP_2:def_1;
then  (a * p) . u9 <> 0. L by Def9;
hence  u in Support (a * p) by POLYNOM1:def_3; ::_thesis: verum
end;
then A15: len z = len y by A1, A5, A11, TARSKI:1;
then A16: dom z = Seg (len y) by FINSEQ_1:def_3
.= dom y by FINSEQ_1:def_3 ;
A17: Support (a * p) = Support p by A13, A11, TARSKI:1;
now__::_thesis:_for_i_being_set_st_i_in_dom_z_holds_
y_/._i_=_a_*_(z_/._i)
A18: dom (a * p) = Bags n by FUNCT_2:def_1;
now__::_thesis:_for_u_being_set_st_u_in_rng_(SgmX_((BagOrder_n),(Support_(a_*_p))))_holds_
u_in_dom_(a_*_p)
let u be set ; ::_thesis: ( u in rng (SgmX ((BagOrder n),(Support (a * p)))) implies u in dom (a * p) )
assume  u in rng (SgmX ((BagOrder n),(Support (a * p)))) ; ::_thesis: u in dom (a * p)
then  u in Support (a * p) by A4, PRE_POLY:def_2;
hence  u in dom (a * p) by A18; ::_thesis: verum
end;
then  rng (SgmX ((BagOrder n),(Support (a * p)))) c= dom (a * p) by TARSKI:def_3;
then reconsider r = (a * p) * (SgmX ((BagOrder n),(Support (a * p)))) as FinSequence by FINSEQ_1:16;
 for u being set st u in rng r holds
u in the carrier of L
proof
let u be set ; ::_thesis: ( u in rng r implies u in the carrier of L )
assume  u in rng r ; ::_thesis: u in the carrier of L
then A19: u in rng (a * p) by FUNCT_1:14;
 rng (a * p) c= the carrier of L by RELAT_1:def_19;
hence  u in the carrier of L by A19; ::_thesis: verum
end;
then A20: rng r c= the carrier of L by TARSKI:def_3;
A21: dom p = Bags n by FUNCT_2:def_1;
now__::_thesis:_for_u_being_set_st_u_in_rng_(SgmX_((BagOrder_n),(Support_(a_*_p))))_holds_
u_in_dom_p
let u be set ; ::_thesis: ( u in rng (SgmX ((BagOrder n),(Support (a * p)))) implies u in dom p )
assume  u in rng (SgmX ((BagOrder n),(Support (a * p)))) ; ::_thesis: u in dom p
then  u in Support (a * p) by A4, PRE_POLY:def_2;
hence  u in dom p by A21; ::_thesis: verum
end;
then  rng (SgmX ((BagOrder n),(Support (a * p)))) c= dom p by TARSKI:def_3;
then reconsider q = p * (SgmX ((BagOrder n),(Support (a * p)))) as FinSequence by FINSEQ_1:16;
 for u being set st u in rng q holds
u in the carrier of L
proof
let u be set ; ::_thesis: ( u in rng q implies u in the carrier of L )
assume  u in rng q ; ::_thesis: u in the carrier of L
then A22: u in rng p by FUNCT_1:14;
 rng p c= the carrier of L by RELAT_1:def_19;
hence  u in the carrier of L by A22; ::_thesis: verum
end;
then A23: rng q c= the carrier of L by TARSKI:def_3;
reconsider r = r as FinSequence of the carrier of L by A20, FINSEQ_1:def_4;
reconsider q = q as FinSequence of the carrier of L by A23, FINSEQ_1:def_4;
let i be set ; ::_thesis: ( i in dom z implies y /. i = a * (z /. i) )
assume A24: i in dom z ; ::_thesis: y /. i = a * (z /. i)
then  i in Seg (len z) by FINSEQ_1:def_3;
then  i in  {  k where k is Element of NAT : ( 1 <= k & k <= len z )  }  by FINSEQ_1:def_1;
then consider k being Element of NAT  such that
A25: i = k and
A26: ( 1 <= k & k <= len z ) ;
A27: dom z = Seg (len (SgmX ((BagOrder n),(Support (a * p))))) by A1, A16, FINSEQ_1:def_3
.= dom (SgmX ((BagOrder n),(Support (a * p)))) by FINSEQ_1:def_3 ;
then  (SgmX ((BagOrder n),(Support (a * p)))) . k = (SgmX ((BagOrder n),(Support (a * p)))) /. k by A24, A25, PARTFUN1:def_6;
then  k in dom q by A24, A25, A27, A21, FUNCT_1:11;
then A28: (p * (SgmX ((BagOrder n),(Support (a * p))))) /. k = q . k by PARTFUN1:def_6
.= p . ((SgmX ((BagOrder n),(Support (a * p)))) . k) by A24, A25, A27, FUNCT_1:13
.= p . ((SgmX ((BagOrder n),(Support (a * p)))) /. k) by A24, A25, A27, PARTFUN1:def_6 ;
reconsider c = (SgmX ((BagOrder n),(Support (a * p)))) /. k as Element of Bags n ;
reconsider c = c as bag of n ;
A29: a * (z /. k) = a * (((p * (SgmX ((BagOrder n),(Support p)))) /. k) * (eval ((((SgmX ((BagOrder n),(Support p))) /. k) @),x))) by A7, A26
.= (a * ((p * (SgmX ((BagOrder n),(Support (a * p))))) /. k)) * (eval ((((SgmX ((BagOrder n),(Support (a * p)))) /. k) @),x)) by A17, GROUP_1:def_3 ;
A30: (a * p) . ((SgmX ((BagOrder n),(Support (a * p)))) /. k) = (a * p) . c
.= a * ((p * (SgmX ((BagOrder n),(Support (a * p))))) /. k) by A28, Def9 ;
 (SgmX ((BagOrder n),(Support (a * p)))) . k = (SgmX ((BagOrder n),(Support (a * p)))) /. k by A24, A25, A27, PARTFUN1:def_6;
then  k in dom r by A24, A25, A27, A18, FUNCT_1:11;
then ((a * p) * (SgmX ((BagOrder n),(Support (a * p))))) /. k = r . k by PARTFUN1:def_6
.= (a * p) . ((SgmX ((BagOrder n),(Support (a * p)))) . k) by A24, A25, A27, FUNCT_1:13
.= a * ((p * (SgmX ((BagOrder n),(Support (a * p))))) /. k) by A24, A25, A27, A30, PARTFUN1:def_6 ;
hence  y /. i = a * (z /. i) by A3, A15, A25, A26, A29; ::_thesis: verum
end;
then  y = a * z by A16, POLYNOM1:def_1;
hence  eval ((a * p),x) = a * (eval (p,x)) by A2, A6, BINOM:4; ::_thesis: verum
end;
end;
end;

theorem :: POLYNOM7:31
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),x) = (eval (p,x)) * a
proof
let n be Ordinal; ::_thesis: 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),x) = (eval (p,x)) * a
let L be non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive left_zeroed doubleLoopStr ; ::_thesis: for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval ((p * a),x) = (eval (p,x)) * a
let p be Polynomial of n,L; ::_thesis: for a being Element of L
for x being Function of n,L holds eval ((p * a),x) = (eval (p,x)) * a
let a be Element of L; ::_thesis: for x being Function of n,L holds eval ((p * a),x) = (eval (p,x)) * a
let x be Function of n,L; ::_thesis: eval ((p * a),x) = (eval (p,x)) * a
thus  eval ((p * a),x) = eval ((p *' (a | (n,L))),x) by Th28
.= (eval (p,x)) * a by Lm5 ; ::_thesis: verum
end;

theorem :: POLYNOM7:32
for n being Ordinal
for L being non trivial left_add-cancelable right_complementable add-associative right_zeroed associative commutative well-unital distributive domRing-like 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),x) = (eval (p,x)) * a
proof
let n be Ordinal; ::_thesis: for L being non trivial left_add-cancelable right_complementable add-associative right_zeroed associative commutative well-unital distributive domRing-like 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),x) = (eval (p,x)) * a
let L be non trivial left_add-cancelable right_complementable add-associative right_zeroed associative commutative well-unital distributive domRing-like left_zeroed doubleLoopStr ; ::_thesis: for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval ((p * a),x) = (eval (p,x)) * a
let p be Polynomial of n,L; ::_thesis: for a being Element of L
for x being Function of n,L holds eval ((p * a),x) = (eval (p,x)) * a
let a be Element of L; ::_thesis: for x being Function of n,L holds eval ((p * a),x) = (eval (p,x)) * a
let x be Function of n,L; ::_thesis: eval ((p * a),x) = (eval (p,x)) * a
consider y being FinSequence of the carrier of L such that
A1: len y = len (SgmX ((BagOrder n),(Support (p * a)))) and
A2: eval ((p * a),x) = Sum y and
A3: for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = (((p * a) * (SgmX ((BagOrder n),(Support (p * a))))) /. i) * (eval ((((SgmX ((BagOrder n),(Support (p * a)))) /. i) @),x)) by POLYNOM2:def_4;
consider z being FinSequence of the carrier of L such that
A4: len z = len (SgmX ((BagOrder n),(Support p))) and
A5: eval (p,x) = Sum z and
A6: for i being Element of NAT st 1 <= i & i <= len z holds
z /. i = ((p * (SgmX ((BagOrder n),(Support p)))) /. i) * (eval ((((SgmX ((BagOrder n),(Support p))) /. i) @),x)) by POLYNOM2:def_4;
now__::_thesis:_(_(_a_=_0._L_&_eval_((p_*_a),x)_=_(eval_(p,x))_*_a_)_or_(_a_<>_0._L_&_eval_((p_*_a),x)_=_(eval_(p,x))_*_a_)_)
percases ( a = 0. L or a <> 0. L ) ;
caseA7: a = 0. L ; ::_thesis: eval ((p * a),x) = (eval (p,x)) * a
A8: now__::_thesis:_for_b_being_bag_of_n_holds_(p_*_a)_._b_=_0._L
let b be bag of n; ::_thesis: (p * a) . b = 0. L
thus (p * a) . b = (p . b) * a by Def10
.= 0. L by A7, BINOM:2 ; ::_thesis: verum
end;
A9: now__::_thesis:_not_Support_(p_*_a)_<>_{}
assume  Support (p * a) <> {} ; ::_thesis: contradiction
then reconsider sp = Support (p * a) as non empty Subset of (Bags n) ;
set c = the Element of sp;
 (p * a) . the Element of sp <> 0. L by POLYNOM1:def_3;
hence  contradiction by A8; ::_thesis: verum
end;
 BagOrder n linearly_orders Support (p * a) by POLYNOM2:18;
then  rng (SgmX ((BagOrder n),(Support (p * a)))) = {} by A9, PRE_POLY:def_2;
then  SgmX ((BagOrder n),(Support (p * a))) = {} by RELAT_1:41;
then  y = <*> the carrier of L by A1;
then  Sum y = 0. L by RLVECT_1:43
.= (Sum z) * a by A7, BINOM:2 ;
hence  eval ((p * a),x) = (eval (p,x)) * a by A2, A5; ::_thesis: verum
end;
caseA10: a <> 0. L ; ::_thesis: eval ((p * a),x) = (eval (p,x)) * a
A11: for u being set st u in Support (p * a) holds
u in Support p
proof
let u be set ; ::_thesis: ( u in Support (p * a) implies u in Support p )
assume A12: u in Support (p * a) ; ::_thesis: u in Support p
then reconsider u9 = u as Element of Bags n ;
 (p * a) . u <> 0. L by A12, POLYNOM1:def_3;
then  (p . u9) * a <> 0. L by Def10;
then  p . u9 <> 0. L by BINOM:1;
hence  u in Support p by POLYNOM1:def_3; ::_thesis: verum
end;
A13: for u being set st u in Support p holds
u in Support (p * a)
proof
let u be set ; ::_thesis: ( u in Support p implies u in Support (p * a) )
assume A14: u in Support p ; ::_thesis: u in Support (p * a)
then reconsider u9 = u as Element of Bags n ;
 p . u <> 0. L by A14, POLYNOM1:def_3;
then  (p . u9) * a <> 0. L by A10, VECTSP_2:def_1;
then  (p * a) . u9 <> 0. L by Def10;
hence  u in Support (p * a) by POLYNOM1:def_3; ::_thesis: verum
end;
then A15: len z = len y by A1, A4, A11, TARSKI:1;
then A16: dom z = Seg (len y) by FINSEQ_1:def_3
.= dom y by FINSEQ_1:def_3 ;
A17: BagOrder n linearly_orders Support (p * a) by POLYNOM2:18;
A18: Support (p * a) = Support p by A13, A11, TARSKI:1;
now__::_thesis:_for_i_being_set_st_i_in_dom_z_holds_
y_/._i_=_(z_/._i)_*_a
A19: dom (p * a) = Bags n by FUNCT_2:def_1;
now__::_thesis:_for_u_being_set_st_u_in_rng_(SgmX_((BagOrder_n),(Support_(p_*_a))))_holds_
u_in_dom_(p_*_a)
let u be set ; ::_thesis: ( u in rng (SgmX ((BagOrder n),(Support (p * a)))) implies u in dom (p * a) )
assume  u in rng (SgmX ((BagOrder n),(Support (p * a)))) ; ::_thesis: u in dom (p * a)
then  u in Support (p * a) by A17, PRE_POLY:def_2;
hence  u in dom (p * a) by A19; ::_thesis: verum
end;
then  rng (SgmX ((BagOrder n),(Support (p * a)))) c= dom (p * a) by TARSKI:def_3;
then reconsider r = (p * a) * (SgmX ((BagOrder n),(Support (p * a)))) as FinSequence by FINSEQ_1:16;
 for u being set st u in rng r holds
u in the carrier of L
proof
let u be set ; ::_thesis: ( u in rng r implies u in the carrier of L )
assume  u in rng r ; ::_thesis: u in the carrier of L
then A20: u in rng (p * a) by FUNCT_1:14;
 rng (p * a) c= the carrier of L by RELAT_1:def_19;
hence  u in the carrier of L by A20; ::_thesis: verum
end;
then A21: rng r c= the carrier of L by TARSKI:def_3;
A22: dom p = Bags n by FUNCT_2:def_1;
now__::_thesis:_for_u_being_set_st_u_in_rng_(SgmX_((BagOrder_n),(Support_(p_*_a))))_holds_
u_in_dom_p
let u be set ; ::_thesis: ( u in rng (SgmX ((BagOrder n),(Support (p * a)))) implies u in dom p )
assume  u in rng (SgmX ((BagOrder n),(Support (p * a)))) ; ::_thesis: u in dom p
then  u in Support (p * a) by A17, PRE_POLY:def_2;
hence  u in dom p by A22; ::_thesis: verum
end;
then  rng (SgmX ((BagOrder n),(Support (p * a)))) c= dom p by TARSKI:def_3;
then reconsider q = p * (SgmX ((BagOrder n),(Support (p * a)))) as FinSequence by FINSEQ_1:16;
 for u being set st u in rng q holds
u in the carrier of L
proof
let u be set ; ::_thesis: ( u in rng q implies u in the carrier of L )
assume  u in rng q ; ::_thesis: u in the carrier of L
then A23: u in rng p by FUNCT_1:14;
 rng p c= the carrier of L by RELAT_1:def_19;
hence  u in the carrier of L by A23; ::_thesis: verum
end;
then A24: rng q c= the carrier of L by TARSKI:def_3;
reconsider r = r as FinSequence of the carrier of L by A21, FINSEQ_1:def_4;
reconsider q = q as FinSequence of the carrier of L by A24, FINSEQ_1:def_4;
let i be set ; ::_thesis: ( i in dom z implies y /. i = (z /. i) * a )
assume A25: i in dom z ; ::_thesis: y /. i = (z /. i) * a
then  i in Seg (len z) by FINSEQ_1:def_3;
then  i in  {  k where k is Element of NAT : ( 1 <= k & k <= len z )  }  by FINSEQ_1:def_1;
then consider k being Element of NAT  such that
A26: i = k and
A27: ( 1 <= k & k <= len z ) ;
A28: dom z = Seg (len (SgmX ((BagOrder n),(Support (p * a))))) by A1, A16, FINSEQ_1:def_3
.= dom (SgmX ((BagOrder n),(Support (p * a)))) by FINSEQ_1:def_3 ;
then  (SgmX ((BagOrder n),(Support (p * a)))) . k = (SgmX ((BagOrder n),(Support (p * a)))) /. k by A25, A26, PARTFUN1:def_6;
then  k in dom q by A25, A26, A28, A22, FUNCT_1:11;
then A29: (p * (SgmX ((BagOrder n),(Support (p * a))))) /. k = q . k by PARTFUN1:def_6
.= p . ((SgmX ((BagOrder n),(Support (p * a)))) . k) by A25, A26, A28, FUNCT_1:13
.= p . ((SgmX ((BagOrder n),(Support (p * a)))) /. k) by A25, A26, A28, PARTFUN1:def_6 ;
reconsider c = (SgmX ((BagOrder n),(Support (p * a)))) /. k as Element of Bags n ;
reconsider c = c as bag of n ;
A30: (z /. k) * a = (((p * (SgmX ((BagOrder n),(Support (p * a))))) /. k) * (eval ((((SgmX ((BagOrder n),(Support (p * a)))) /. k) @),x))) * a by A6, A18, A27
.= (((p * (SgmX ((BagOrder n),(Support (p * a))))) /. k) * a) * (eval ((((SgmX ((BagOrder n),(Support (p * a)))) /. k) @),x)) by GROUP_1:def_3 ;
A31: (p * a) . ((SgmX ((BagOrder n),(Support (p * a)))) /. k) = (p * a) . c
.= ((p * (SgmX ((BagOrder n),(Support (p * a))))) /. k) * a by A29, Def10 ;
 (SgmX ((BagOrder n),(Support (p * a)))) . k = (SgmX ((BagOrder n),(Support (p * a)))) /. k by A25, A26, A28, PARTFUN1:def_6;
then  k in dom r by A25, A26, A28, A19, FUNCT_1:11;
then ((p * a) * (SgmX ((BagOrder n),(Support (p * a))))) /. k = r . k by PARTFUN1:def_6
.= (p * a) . ((SgmX ((BagOrder n),(Support (p * a)))) . k) by A25, A26, A28, FUNCT_1:13
.= ((p * (SgmX ((BagOrder n),(Support (p * a))))) /. k) * a by A25, A26, A28, A31, PARTFUN1:def_6 ;
hence  y /. i = (z /. i) * a by A3, A15, A26, A27, A30; ::_thesis: verum
end;
then  y = z * a by A16, POLYNOM1:def_2;
hence  eval ((p * a),x) = (eval (p,x)) * a by A2, A5, BINOM:5; ::_thesis: verum
end;
end;
end;
hence  eval ((p * a),x) = (eval (p,x)) * a ; ::_thesis: verum
end;

theorem :: POLYNOM7:33
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)) by Lm4;

theorem :: POLYNOM7:34
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
proof
let n be Ordinal; ::_thesis: 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
let L be non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive left_zeroed doubleLoopStr ; ::_thesis: 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
let p be Polynomial of n,L; ::_thesis: for a being Element of L
for x being Function of n,L holds eval ((p *' (a | (n,L))),x) = (eval (p,x)) * a
let a be Element of L; ::_thesis: for x being Function of n,L holds eval ((p *' (a | (n,L))),x) = (eval (p,x)) * a
let x be Function of n,L; ::_thesis: eval ((p *' (a | (n,L))),x) = (eval (p,x)) * a
thus  eval ((p *' (a | (n,L))),x) = (eval (p,x)) * (eval ((a | (n,L)),x)) by POLYNOM2:25
.= (eval (p,x)) * a by Th25 ; ::_thesis: verum
end;