:: TERMORD semantic presentation begin registration cluster non trivial for addLoopStr ; existence not for b1 being addLoopStr holds b1 is trivial proof take the Field ; ::_thesis: not the Field is trivial thus not the Field is trivial ; ::_thesis: verum end; end; registration cluster non empty non trivial right_complementable add-associative right_zeroed for addLoopStr ; existence ex b1 being non trivial addLoopStr st ( b1 is add-associative & b1 is right_complementable & b1 is right_zeroed ) proof set F = the Field; take the Field ; ::_thesis: ( the Field is add-associative & the Field is right_complementable & the Field is right_zeroed ) thus ( the Field is add-associative & the Field is right_complementable & the Field is right_zeroed ) ; ::_thesis: verum end; end; definition let X be set ; let b be bag of X; attrb is zero means :: TERMORD:def 1 b = EmptyBag X; end; :: deftheorem defines zero TERMORD:def_1_:_ for X being set for b being bag of X holds ( b is zero iff b = EmptyBag X ); theorem Th1: :: TERMORD:1 for X being set for b1, b2 being bag of X holds ( b1 divides b2 iff ex b being bag of X st b2 = b1 + b ) proof let n be set ; ::_thesis: for b1, b2 being bag of n holds ( b1 divides b2 iff ex b being bag of n st b2 = b1 + b ) let b1, b2 be bag of n; ::_thesis: ( b1 divides b2 iff ex b being bag of n st b2 = b1 + b ) now__::_thesis:_(_b1_divides_b2_implies_ex_b_being_bag_of_n_st_b2_=_b1_+_b_) assume A1: b1 divides b2 ; ::_thesis: ex b being bag of n st b2 = b1 + b A2: now__::_thesis:_for_k_being_set_holds_0_<=_(b2_._k)_-_(b1_._k) let k be set ; ::_thesis: 0 <= (b2 . k) - (b1 . k) b1 . k <= b2 . k by A1, PRE_POLY:def_11; then (b1 . k) - (b1 . k) <= (b2 . k) - (b1 . k) by XREAL_1:9; hence 0 <= (b2 . k) - (b1 . k) ; ::_thesis: verum end; now__::_thesis:_(_(_n_=_{}_&_ex_b_being_bag_of_n_st_b2_=_b1_+_b_)_or_(_n_<>_{}_&_ex_b,_b_being_bag_of_n_st_b2_=_b1_+_b_)_) percases ( n = {} or n <> {} ) ; caseA3: n = {} ; ::_thesis: ex b being bag of n st b2 = b1 + b then b1 + (EmptyBag n) = EmptyBag n by POLYNOM7:3 .= b2 by A3, POLYNOM7:3 ; hence ex b being bag of n st b2 = b1 + b ; ::_thesis: verum end; case n <> {} ; ::_thesis: ex b, b being bag of n st b2 = b1 + b then reconsider n9 = n as non empty set ; set b = { [k,((b2 . k) -' (b1 . k))] where k is Element of n9 : verum } ; A4: now__::_thesis:_for_x_being_set_st_x_in__{__[k,((b2_._k)_-'_(b1_._k))]_where_k_is_Element_of_n9_:_verum__}__holds_ ex_y,_z_being_set_st_x_=_[y,z] let x be set ; ::_thesis: ( x in { [k,((b2 . k) -' (b1 . k))] where k is Element of n9 : verum } implies ex y, z being set st x = [y,z] ) assume x in { [k,((b2 . k) -' (b1 . k))] where k is Element of n9 : verum } ; ::_thesis: ex y, z being set st x = [y,z] then ex k being Element of n9 st x = [k,((b2 . k) -' (b1 . k))] ; hence ex y, z being set st x = [y,z] ; ::_thesis: verum end; now__::_thesis:_for_x,_y1,_y2_being_set_st_[x,y1]_in__{__[k,((b2_._k)_-'_(b1_._k))]_where_k_is_Element_of_n9_:_verum__}__&_[x,y2]_in__{__[k,((b2_._k)_-'_(b1_._k))]_where_k_is_Element_of_n9_:_verum__}__holds_ y1_=_y2 let x, y1, y2 be set ; ::_thesis: ( [x,y1] in { [k,((b2 . k) -' (b1 . k))] where k is Element of n9 : verum } & [x,y2] in { [k,((b2 . k) -' (b1 . k))] where k is Element of n9 : verum } implies y1 = y2 ) assume that A5: [x,y1] in { [k,((b2 . k) -' (b1 . k))] where k is Element of n9 : verum } and A6: [x,y2] in { [k,((b2 . k) -' (b1 . k))] where k is Element of n9 : verum } ; ::_thesis: y1 = y2 consider k being Element of n9 such that A7: [x,y1] = [k,((b2 . k) -' (b1 . k))] by A5; consider k9 being Element of n9 such that A8: [x,y2] = [k9,((b2 . k9) -' (b1 . k9))] by A6; k = x by A7, XTUPLE_0:1 .= k9 by A8, XTUPLE_0:1 ; hence y1 = y2 by A7, A8, XTUPLE_0:1; ::_thesis: verum end; then reconsider b = { [k,((b2 . k) -' (b1 . k))] where k is Element of n9 : verum } as Function by A4, FUNCT_1:def_1, RELAT_1:def_1; A9: now__::_thesis:_for_x_being_set_st_x_in_dom_b_holds_ x_in_n9 let x be set ; ::_thesis: ( x in dom b implies x in n9 ) assume x in dom b ; ::_thesis: x in n9 then consider y being set such that A10: [x,y] in b by XTUPLE_0:def_12; consider k being Element of n9 such that A11: [x,y] = [k,((b2 . k) -' (b1 . k))] by A10; x = k by A11, XTUPLE_0:1; hence x in n9 ; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_n9_holds_ x_in_dom_b let x be set ; ::_thesis: ( x in n9 implies x in dom b ) assume x in n9 ; ::_thesis: x in dom b then reconsider k = x as Element of n9 ; [k,((b2 . k) -' (b1 . k))] in b ; hence x in dom b by XTUPLE_0:def_12; ::_thesis: verum end; then A12: dom b = n9 by A9, TARSKI:1; then reconsider b = b as ManySortedSet of n9 by PARTFUN1:def_2, RELAT_1:def_18; A13: now__::_thesis:_for_k_being_set_st_k_in_n_holds_ b_._k_=_(b2_._k)_-'_(b1_._k) let k be set ; ::_thesis: ( k in n implies b . k = (b2 . k) -' (b1 . k) ) assume k in n ; ::_thesis: b . k = (b2 . k) -' (b1 . k) then consider u being set such that A14: [k,u] in b by A12, XTUPLE_0:def_12; consider k9 being Element of n9 such that A15: [k,u] = [k9,((b2 . k9) -' (b1 . k9))] by A14; A16: u = (b2 . k9) -' (b1 . k9) by A15, XTUPLE_0:1; k = k9 by A15, XTUPLE_0:1; hence b . k = (b2 . k) -' (b1 . k) by A14, A16, FUNCT_1:1; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_support_b_holds_ x_in_support_b2 let x be set ; ::_thesis: ( x in support b implies x in support b2 ) A17: support b c= dom b by PRE_POLY:37; assume A18: x in support b ; ::_thesis: x in support b2 then A19: b . x <> 0 by PRE_POLY:def_7; now__::_thesis:_x_in_support_b2 assume not x in support b2 ; ::_thesis: contradiction then b2 . x = 0 by PRE_POLY:def_7; then 0 = (b2 . x) -' (b1 . x) by NAT_2:8; hence contradiction by A12, A13, A18, A19, A17; ::_thesis: verum end; hence x in support b2 ; ::_thesis: verum end; then A20: support b c= support b2 by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_rng_b_holds_ x_in_NAT let x be set ; ::_thesis: ( x in rng b implies x in NAT ) assume x in rng b ; ::_thesis: x in NAT then consider y being set such that A21: [y,x] in b by XTUPLE_0:def_13; consider k being Element of n9 such that A22: [y,x] = [k,((b2 . k) -' (b1 . k))] by A21; x = (b2 . k) -' (b1 . k) by A22, XTUPLE_0:1; hence x in NAT ; ::_thesis: verum end; then rng b c= NAT by TARSKI:def_3; then reconsider b = b as bag of n by A20, PRE_POLY:def_8, VALUED_0:def_6; take b = b; ::_thesis: ex b being bag of n st b2 = b1 + b now__::_thesis:_for_k_being_set_st_k_in_n_holds_ (b1_._k)_+_(b_._k)_=_b2_._k let k be set ; ::_thesis: ( k in n implies (b1 . k) + (b . k) = b2 . k ) A23: 0 <= (b2 . k) - (b1 . k) by A2; assume k in n ; ::_thesis: (b1 . k) + (b . k) = b2 . k hence (b1 . k) + (b . k) = (b1 . k) + ((b2 . k) -' (b1 . k)) by A13 .= (b1 . k) + ((b2 . k) + (- (b1 . k))) by A23, XREAL_0:def_2 .= b2 . k ; ::_thesis: verum end; then b2 = b1 + b by PRE_POLY:33; hence ex b being bag of n st b2 = b1 + b ; ::_thesis: verum end; end; end; hence ex b being bag of n st b2 = b1 + b ; ::_thesis: verum end; hence ( b1 divides b2 iff ex b being bag of n st b2 = b1 + b ) by PRE_POLY:50; ::_thesis: verum end; theorem Th2: :: TERMORD:2 for n being Ordinal for L being non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr for p being Series of n,L holds (0_ (n,L)) *' p = 0_ (n,L) proof let n be Ordinal; ::_thesis: for L being non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr for p being Series of n,L holds (0_ (n,L)) *' p = 0_ (n,L) let L be non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Series of n,L holds (0_ (n,L)) *' p = 0_ (n,L) let p be Series of n,L; ::_thesis: (0_ (n,L)) *' p = 0_ (n,L) set Z = 0_ (n,L); now__::_thesis:_for_b_being_Element_of_Bags_n_holds_((0__(n,L))_*'_p)_._b_=_(0__(n,L))_._b let b be Element of Bags n; ::_thesis: ((0_ (n,L)) *' p) . b = (0_ (n,L)) . b consider s being FinSequence of L such that A1: ((0_ (n,L)) *' p) . b = Sum s and len s = len (decomp b) and A2: 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 = ((0_ (n,L)) . b1) * (p . b2) ) by POLYNOM1:def_9; now__::_thesis:_for_k_being_Nat_st_k_in_dom_s_holds_ s_/._k_=_0._L let k be Nat; ::_thesis: ( k in dom s implies s /. k = 0. L ) assume k in dom s ; ::_thesis: s /. k = 0. L then consider b1, b2 being bag of n such that (decomp b) /. k = <*b1,b2*> and A3: s /. k = ((0_ (n,L)) . b1) * (p . b2) by A2; thus s /. k = (0. L) * (p . b2) by A3, POLYNOM1:22 .= 0. L by VECTSP_1:7 ; ::_thesis: verum end; then Sum s = 0. L by MATRLIN:11; hence ((0_ (n,L)) *' p) . b = (0_ (n,L)) . b by A1, POLYNOM1:22; ::_thesis: verum end; hence (0_ (n,L)) *' p = 0_ (n,L) by FUNCT_2:63; ::_thesis: verum end; registration let n be Ordinal; let L be non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; let m1, m2 be Monomial of n,L; clusterm1 *' m2 -> monomial-like ; coherence m1 *' m2 is monomial-like proof percases ( Support (m1 *' m2) = {} or Support (m1 *' m2) <> {} ) ; suppose Support (m1 *' m2) = {} ; ::_thesis: m1 *' m2 is monomial-like hence m1 *' m2 is monomial-like by POLYNOM7:6; ::_thesis: verum end; supposeA1: Support (m1 *' m2) <> {} ; ::_thesis: m1 *' m2 is monomial-like now__::_thesis:_(_(_Support_m1_<>_{}_&_Support_m2_<>_{}_&_m1_*'_m2_is_monomial-like_)_or_(_(_Support_m1_=_{}_or_Support_m2_=_{}_)_&_m1_*'_m2_is_monomial-like_)_) percases ( ( Support m1 <> {} & Support m2 <> {} ) or Support m1 = {} or Support m2 = {} ) ; caseA2: ( Support m1 <> {} & Support m2 <> {} ) ; ::_thesis: m1 *' m2 is monomial-like then consider mb2 being bag of n such that A3: Support m2 = {mb2} by POLYNOM7:6; mb2 in Support m2 by A3, TARSKI:def_1; then A4: m2 . mb2 <> 0. L by POLYNOM1:def_3; A5: now__::_thesis:_for_b_being_bag_of_n_st_b_<>_mb2_holds_ m2_._b_=_0._L let b be bag of n; ::_thesis: ( b <> mb2 implies m2 . b = 0. L ) assume A6: b <> mb2 ; ::_thesis: m2 . b = 0. L consider b9 being bag of n such that A7: for b being bag of n st b <> b9 holds m2 . b = 0. L by POLYNOM7:def_3; b9 = mb2 by A4, A7; hence m2 . b = 0. L by A6, A7; ::_thesis: verum end; consider mb1 being bag of n such that A8: Support m1 = {mb1} by A2, POLYNOM7:6; mb1 in Support m1 by A8, TARSKI:def_1; then A9: m1 . mb1 <> 0. L by POLYNOM1:def_3; A10: now__::_thesis:_for_b_being_bag_of_n_st_b_<>_mb1_holds_ m1_._b_=_0._L let b be bag of n; ::_thesis: ( b <> mb1 implies m1 . b = 0. L ) assume A11: b <> mb1 ; ::_thesis: m1 . b = 0. L consider b9 being bag of n such that A12: for b being bag of n st b <> b9 holds m1 . b = 0. L by POLYNOM7:def_3; b9 = mb1 by A9, A12; hence m1 . b = 0. L by A11, A12; ::_thesis: verum end; set b = the Element of Support (m1 *' m2); A13: the Element of Support (m1 *' m2) in Support (m1 *' m2) by A1; then the Element of Support (m1 *' m2) is Element of Bags n ; then reconsider b = the Element of Support (m1 *' m2) as bag of n ; consider s being FinSequence of L such that A14: (m1 *' m2) . b = Sum s and A15: len s = len (decomp b) and A16: 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 = (m1 . b1) * (m2 . b2) ) by POLYNOM1:def_9; A17: dom s = Seg (len (decomp b)) by A15, FINSEQ_1:def_3 .= dom (decomp b) by FINSEQ_1:def_3 ; A18: now__::_thesis:_not_b_<>_mb1_+_mb2 assume A19: b <> mb1 + mb2 ; ::_thesis: contradiction A20: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_s_holds_ s_/._k_=_0._L let k be Element of NAT ; ::_thesis: ( k in dom s implies s /. k = 0. L ) assume A21: k in dom s ; ::_thesis: s /. k = 0. L then consider b1, b2 being bag of n such that A22: (decomp b) /. k = <*b1,b2*> and A23: s /. k = (m1 . b1) * (m2 . b2) by A16; consider b19, b29 being bag of n such that A24: (decomp b) /. k = <*b19,b29*> and A25: b = b19 + b29 by A17, A21, PRE_POLY:68; A26: b2 = <*b19,b29*> . 2 by A22, A24, FINSEQ_1:44 .= b29 by FINSEQ_1:44 ; A27: b1 = <*b19,b29*> . 1 by A22, A24, FINSEQ_1:44 .= b19 by FINSEQ_1:44 ; now__::_thesis:_(_(_b1_<>_mb1_&_(m1_._b1)_*_(m2_._b2)_=_0._L_)_or_(_b2_<>_mb2_&_(m1_._b1)_*_(m2_._b2)_=_0._L_)_) percases ( b1 <> mb1 or b2 <> mb2 ) by A19, A25, A27, A26; case b1 <> mb1 ; ::_thesis: (m1 . b1) * (m2 . b2) = 0. L then m1 . b1 = 0. L by A10; hence (m1 . b1) * (m2 . b2) = 0. L by BINOM:1; ::_thesis: verum end; case b2 <> mb2 ; ::_thesis: (m1 . b1) * (m2 . b2) = 0. L then m2 . b2 = 0. L by A5; hence (m1 . b1) * (m2 . b2) = 0. L by BINOM:2; ::_thesis: verum end; end; end; hence s /. k = 0. L by A23; ::_thesis: verum end; now__::_thesis:_(_(_dom_s_=_{}_&_(m1_*'_m2)_._b_=_0._L_)_or_(_dom_s_<>_{}_&_(m1_*'_m2)_._b_=_0._L_)_) percases ( dom s = {} or dom s <> {} ) ; case dom s = {} ; ::_thesis: (m1 *' m2) . b = 0. L then s = <*> the carrier of L by RELAT_1:41; hence (m1 *' m2) . b = 0. L by A15; ::_thesis: verum end; caseA28: dom s <> {} ; ::_thesis: (m1 *' m2) . b = 0. L set k = the Element of dom s; A29: the Element of dom s in dom s by A28; for k9 being Element of NAT st k9 in dom s & k9 <> the Element of dom s holds s /. k9 = 0. L by A20; then s /. the Element of dom s = (m1 *' m2) . b by A14, A29, POLYNOM2:3; hence (m1 *' m2) . b = 0. L by A20, A29; ::_thesis: verum end; end; end; hence contradiction by A13, POLYNOM1:def_3; ::_thesis: verum end; now__::_thesis:_for_b9_being_bag_of_n_st_b9_<>_b_holds_ (m1_*'_m2)_._b9_=_0._L let b9 be bag of n; ::_thesis: ( b9 <> b implies (m1 *' m2) . b9 = 0. L ) assume A30: b9 <> b ; ::_thesis: (m1 *' m2) . b9 = 0. L consider s being FinSequence of L such that A31: (m1 *' m2) . b9 = Sum s and A32: len s = len (decomp b9) and A33: for k being Element of NAT st k in dom s holds ex b1, b2 being bag of n st ( (decomp b9) /. k = <*b1,b2*> & s /. k = (m1 . b1) * (m2 . b2) ) by POLYNOM1:def_9; A34: dom s = Seg (len (decomp b9)) by A32, FINSEQ_1:def_3 .= dom (decomp b9) by FINSEQ_1:def_3 ; A35: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_s_holds_ s_/._k_=_0._L let k be Element of NAT ; ::_thesis: ( k in dom s implies s /. k = 0. L ) assume A36: k in dom s ; ::_thesis: s /. k = 0. L then consider b1, b2 being bag of n such that A37: (decomp b9) /. k = <*b1,b2*> and A38: s /. k = (m1 . b1) * (m2 . b2) by A33; consider b19, b29 being bag of n such that A39: (decomp b9) /. k = <*b19,b29*> and A40: b9 = b19 + b29 by A34, A36, PRE_POLY:68; A41: b2 = <*b19,b29*> . 2 by A37, A39, FINSEQ_1:44 .= b29 by FINSEQ_1:44 ; A42: b1 = <*b19,b29*> . 1 by A37, A39, FINSEQ_1:44 .= b19 by FINSEQ_1:44 ; now__::_thesis:_(_(_b1_<>_mb1_&_(m1_._b1)_*_(m2_._b2)_=_0._L_)_or_(_b2_<>_mb2_&_(m1_._b1)_*_(m2_._b2)_=_0._L_)_) percases ( b1 <> mb1 or b2 <> mb2 ) by A18, A30, A40, A42, A41; case b1 <> mb1 ; ::_thesis: (m1 . b1) * (m2 . b2) = 0. L then m1 . b1 = 0. L by A10; hence (m1 . b1) * (m2 . b2) = 0. L by BINOM:1; ::_thesis: verum end; case b2 <> mb2 ; ::_thesis: (m1 . b1) * (m2 . b2) = 0. L then m2 . b2 = 0. L by A5; hence (m1 . b1) * (m2 . b2) = 0. L by BINOM:2; ::_thesis: verum end; end; end; hence s /. k = 0. L by A38; ::_thesis: verum end; now__::_thesis:_(_(_dom_s_=_{}_&_(m1_*'_m2)_._b9_=_0._L_)_or_(_dom_s_<>_{}_&_(m1_*'_m2)_._b9_=_0._L_)_) percases ( dom s = {} or dom s <> {} ) ; case dom s = {} ; ::_thesis: (m1 *' m2) . b9 = 0. L then s = <*> the carrier of L by RELAT_1:41; hence (m1 *' m2) . b9 = 0. L by A32; ::_thesis: verum end; caseA43: dom s <> {} ; ::_thesis: (m1 *' m2) . b9 = 0. L set k = the Element of dom s; A44: the Element of dom s in dom s by A43; for k9 being Element of NAT st k9 in dom s & k9 <> the Element of dom s holds s /. k9 = 0. L by A35; then s /. the Element of dom s = (m1 *' m2) . b9 by A31, A44, POLYNOM2:3; hence (m1 *' m2) . b9 = 0. L by A35, A44; ::_thesis: verum end; end; end; hence (m1 *' m2) . b9 = 0. L ; ::_thesis: verum end; hence m1 *' m2 is monomial-like by POLYNOM7:def_3; ::_thesis: verum end; caseA45: ( Support m1 = {} or Support m2 = {} ) ; ::_thesis: m1 *' m2 is monomial-like now__::_thesis:_(_(_Support_m1_=_{}_&_m1_*'_m2_is_monomial-like_)_or_(_Support_m2_=_{}_&_m1_*'_m2_is_monomial-like_)_) percases ( Support m1 = {} or Support m2 = {} ) by A45; case Support m1 = {} ; ::_thesis: m1 *' m2 is monomial-like then m1 = 0_ (n,L) by POLYNOM7:1; hence m1 *' m2 is monomial-like by Th2; ::_thesis: verum end; case Support m2 = {} ; ::_thesis: m1 *' m2 is monomial-like then m2 = 0_ (n,L) by POLYNOM7:1; hence m1 *' m2 is monomial-like by POLYNOM1:28; ::_thesis: verum end; end; end; hence m1 *' m2 is monomial-like ; ::_thesis: verum end; end; end; hence m1 *' m2 is monomial-like ; ::_thesis: verum end; end; end; end; registration let n be Ordinal; let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; let c1, c2 be ConstPoly of n,L; clusterc1 *' c2 -> Constant ; coherence c1 *' c2 is Constant proof set p = c1 *' c2; now__::_thesis:_for_b_being_bag_of_n_st_b_<>_EmptyBag_n_holds_ (c1_*'_c2)_._b_=_0._L let b be bag of n; ::_thesis: ( b <> EmptyBag n implies (c1 *' c2) . b = 0. L ) assume A1: b <> EmptyBag n ; ::_thesis: (c1 *' c2) . b = 0. L consider s being FinSequence of L such that A2: (c1 *' c2) . b = Sum s and A3: len s = len (decomp b) and A4: 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 = (c1 . b1) * (c2 . b2) ) by POLYNOM1:def_9; A5: dom s = Seg (len (decomp b)) by A3, FINSEQ_1:def_3 .= dom (decomp b) by FINSEQ_1:def_3 ; A6: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_s_holds_ s_/._k_=_0._L let k be Element of NAT ; ::_thesis: ( k in dom s implies s /. k = 0. L ) assume A7: k in dom s ; ::_thesis: s /. k = 0. L then consider b1, b2 being bag of n such that A8: (decomp b) /. k = <*b1,b2*> and A9: s /. k = (c1 . b1) * (c2 . b2) by A4; consider b19, b29 being bag of n such that A10: (decomp b) /. k = <*b19,b29*> and A11: b = b19 + b29 by A5, A7, PRE_POLY:68; A12: b2 = <*b19,b29*> . 2 by A8, A10, FINSEQ_1:44 .= b29 by FINSEQ_1:44 ; b1 = <*b19,b29*> . 1 by A8, A10, FINSEQ_1:44 .= b19 by FINSEQ_1:44 ; then A13: ( b1 <> EmptyBag n or b2 <> EmptyBag n ) by A1, A11, A12, PRE_POLY:53; now__::_thesis:_(_(_c1_._b1_=_0._L_&_s_/._k_=_0._L_)_or_(_c2_._b2_=_0._L_&_s_/._k_=_0._L_)_) percases ( c1 . b1 = 0. L or c2 . b2 = 0. L ) by A13, POLYNOM7:def_7; case c1 . b1 = 0. L ; ::_thesis: s /. k = 0. L hence s /. k = 0. L by A9, BINOM:1; ::_thesis: verum end; case c2 . b2 = 0. L ; ::_thesis: s /. k = 0. L hence s /. k = 0. L by A9, BINOM:2; ::_thesis: verum end; end; end; hence s /. k = 0. L ; ::_thesis: verum end; now__::_thesis:_(_(_dom_s_=_{}_&_(c1_*'_c2)_._b_=_0._L_)_or_(_dom_s_<>_{}_&_(c1_*'_c2)_._b_=_0._L_)_) percases ( dom s = {} or dom s <> {} ) ; case dom s = {} ; ::_thesis: (c1 *' c2) . b = 0. L then s = <*> the carrier of L by RELAT_1:41; hence (c1 *' c2) . b = 0. L by A3; ::_thesis: verum end; caseA14: dom s <> {} ; ::_thesis: (c1 *' c2) . b = 0. L set k = the Element of dom s; A15: the Element of dom s in dom s by A14; for k9 being Element of NAT st k9 in dom s & k9 <> the Element of dom s holds s /. k9 = 0. L by A6; then Sum s = s /. the Element of dom s by A15, POLYNOM2:3; hence (c1 *' c2) . b = 0. L by A2, A6, A15; ::_thesis: verum end; end; end; hence (c1 *' c2) . b = 0. L ; ::_thesis: verum end; hence c1 *' c2 is Constant by POLYNOM7:def_7; ::_thesis: verum end; end; theorem Th3: :: TERMORD:3 for n being Ordinal for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr for b, b9 being bag of n for a, a9 being non zero Element of L holds Monom ((a * a9),(b + b9)) = (Monom (a,b)) *' (Monom (a9,b9)) proof let n be Ordinal; ::_thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr for b, b9 being bag of n for a, a9 being non zero Element of L holds Monom ((a * a9),(b + b9)) = (Monom (a,b)) *' (Monom (a9,b9)) let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for b, b9 being bag of n for a, a9 being non zero Element of L holds Monom ((a * a9),(b + b9)) = (Monom (a,b)) *' (Monom (a9,b9)) let b, b9 be bag of n; ::_thesis: for a, a9 being non zero Element of L holds Monom ((a * a9),(b + b9)) = (Monom (a,b)) *' (Monom (a9,b9)) let a, a9 be non zero Element of L; ::_thesis: Monom ((a * a9),(b + b9)) = (Monom (a,b)) *' (Monom (a9,b9)) set m1 = Monom (a,b); set m2 = Monom (a9,b9); set m = Monom ((a * a9),(b + b9)); set m3 = (Monom (a,b)) *' (Monom (a9,b9)); consider s being FinSequence of L such that A1: ((Monom (a,b)) *' (Monom (a9,b9))) . (b + b9) = Sum s and A2: len s = len (decomp (b + b9)) and A3: for k being Element of NAT st k in dom s holds ex b1, b2 being bag of n st ( (decomp (b + b9)) /. k = <*b1,b2*> & s /. k = ((Monom (a,b)) . b1) * ((Monom (a9,b9)) . b2) ) by POLYNOM1:def_9; set u = b + b9; consider k9 being Element of NAT such that A4: k9 in dom (decomp (b + b9)) and A5: (decomp (b + b9)) /. k9 = <*b,b9*> by PRE_POLY:69; A6: dom s = Seg (len (decomp (b + b9))) by A2, FINSEQ_1:def_3 .= dom (decomp (b + b9)) by FINSEQ_1:def_3 ; then consider b1, b2 being bag of n such that A7: (decomp (b + b9)) /. k9 = <*b1,b2*> and A8: s /. k9 = ((Monom (a,b)) . b1) * ((Monom (a9,b9)) . b2) by A3, A4; A9: b1 = <*b,b9*> . 1 by A5, A7, FINSEQ_1:44 .= b by FINSEQ_1:44 ; A10: b2 = <*b,b9*> . 2 by A5, A7, FINSEQ_1:44 .= b9 by FINSEQ_1:44 ; A11: (Monom (a9,b9)) . b9 = (Monom (a9,b9)) . (term (Monom (a9,b9))) by POLYNOM7:10 .= coefficient (Monom (a9,b9)) by POLYNOM7:def_6 .= a9 by POLYNOM7:9 ; A12: now__::_thesis:_for_u_being_bag_of_n_st_u_<>_b9_holds_ not_(Monom_(a9,b9))_._u_<>_0._L A13: (Monom (a9,b9)) . b9 <> 0. L by A11; let u be bag of n; ::_thesis: ( u <> b9 implies not (Monom (a9,b9)) . u <> 0. L ) assume A14: u <> b9 ; ::_thesis: not (Monom (a9,b9)) . u <> 0. L consider v being bag of n such that A15: for b9 being bag of n st b9 <> v holds (Monom (a9,b9)) . b9 = 0. L by POLYNOM7:def_3; assume (Monom (a9,b9)) . u <> 0. L ; ::_thesis: contradiction then u = v by A15; hence contradiction by A14, A15, A13; ::_thesis: verum end; a * a9 <> 0. L by VECTSP_2:def_1; then A16: not a * a9 is zero by STRUCT_0:def_12; A17: (Monom (a,b)) . b = (Monom (a,b)) . (term (Monom (a,b))) by POLYNOM7:10 .= coefficient (Monom (a,b)) by POLYNOM7:def_6 .= a by POLYNOM7:9 ; A18: now__::_thesis:_for_u_being_bag_of_n_st_u_<>_b_holds_ not_(Monom_(a,b))_._u_<>_0._L A19: (Monom (a,b)) . b <> 0. L by A17; let u be bag of n; ::_thesis: ( u <> b implies not (Monom (a,b)) . u <> 0. L ) assume A20: u <> b ; ::_thesis: not (Monom (a,b)) . u <> 0. L consider v being bag of n such that A21: for b9 being bag of n st b9 <> v holds (Monom (a,b)) . b9 = 0. L by POLYNOM7:def_3; assume (Monom (a,b)) . u <> 0. L ; ::_thesis: contradiction then u = v by A21; hence contradiction by A20, A21, A19; ::_thesis: verum end; A22: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_s_&_k_<>_k9_holds_ s_/._k_=_0._L let k be Element of NAT ; ::_thesis: ( k in dom s & k <> k9 implies s /. k = 0. L ) assume that A23: k in dom s and A24: k <> k9 ; ::_thesis: s /. k = 0. L consider b1, b2 being bag of n such that A25: (decomp (b + b9)) /. k = <*b1,b2*> and A26: s /. k = ((Monom (a,b)) . b1) * ((Monom (a9,b9)) . b2) by A3, A23; A27: now__::_thesis:_(_b1_=_b_implies_not_b2_=_b9_) assume A28: ( b1 = b & b2 = b9 ) ; ::_thesis: contradiction (decomp (b + b9)) . k = (decomp (b + b9)) /. k by A6, A23, PARTFUN1:def_6 .= (decomp (b + b9)) . k9 by A4, A5, A25, A28, PARTFUN1:def_6 ; hence contradiction by A6, A4, A23, A24, FUNCT_1:def_4; ::_thesis: verum end; now__::_thesis:_(_(_b1_<>_b_&_((Monom_(a,b))_._b1)_*_((Monom_(a9,b9))_._b2)_=_0._L_)_or_(_b2_<>_b9_&_((Monom_(a,b))_._b1)_*_((Monom_(a9,b9))_._b2)_=_0._L_)_) percases ( b1 <> b or b2 <> b9 ) by A27; case b1 <> b ; ::_thesis: ((Monom (a,b)) . b1) * ((Monom (a9,b9)) . b2) = 0. L then (Monom (a,b)) . b1 = 0. L by A18; hence ((Monom (a,b)) . b1) * ((Monom (a9,b9)) . b2) = 0. L by BINOM:1; ::_thesis: verum end; case b2 <> b9 ; ::_thesis: ((Monom (a,b)) . b1) * ((Monom (a9,b9)) . b2) = 0. L then (Monom (a9,b9)) . b2 = 0. L by A12; hence ((Monom (a,b)) . b1) * ((Monom (a9,b9)) . b2) = 0. L by BINOM:2; ::_thesis: verum end; end; end; hence s /. k = 0. L by A26; ::_thesis: verum end; then Sum s = s /. k9 by A6, A4, POLYNOM2:3; then A29: ((Monom (a,b)) *' (Monom (a9,b9))) . (b + b9) <> 0. L by A17, A11, A1, A8, A9, A10, VECTSP_2:def_1; then A30: term ((Monom (a,b)) *' (Monom (a9,b9))) = b + b9 by POLYNOM7:def_5 .= term (Monom ((a * a9),(b + b9))) by A16, POLYNOM7:10 ; A31: coefficient ((Monom (a,b)) *' (Monom (a9,b9))) = ((Monom (a,b)) *' (Monom (a9,b9))) . (term ((Monom (a,b)) *' (Monom (a9,b9)))) by POLYNOM7:def_6 .= ((Monom (a,b)) *' (Monom (a9,b9))) . (b + b9) by A29, POLYNOM7:def_5 .= a * a9 by A17, A11, A1, A6, A4, A8, A9, A10, A22, POLYNOM2:3 .= coefficient (Monom ((a * a9),(b + b9))) by POLYNOM7:9 ; thus Monom ((a * a9),(b + b9)) = Monom ((coefficient (Monom ((a * a9),(b + b9)))),(term (Monom ((a * a9),(b + b9))))) by POLYNOM7:11 .= (Monom (a,b)) *' (Monom (a9,b9)) by A30, A31, POLYNOM7:11 ; ::_thesis: verum end; theorem :: TERMORD:4 for n being Ordinal for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr for a, a9 being Element of L holds (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L)) proof let n be Ordinal; ::_thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr for a, a9 being Element of L holds (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L)) let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for a, a9 being Element of L holds (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L)) let a, a9 be Element of L; ::_thesis: (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L)) percases ( ( not a is zero & not a9 is zero ) or a is zero or a9 is zero ) ; supposeA1: ( not a is zero & not a9 is zero ) ; ::_thesis: (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L)) ( term ((a * a9) | (n,L)) = EmptyBag n & coefficient ((a * a9) | (n,L)) = a * a9 ) by POLYNOM7:23; then A2: (a * a9) | (n,L) = Monom ((a * a9),(EmptyBag n)) by POLYNOM7:11; ( term (a9 | (n,L)) = EmptyBag n & coefficient (a9 | (n,L)) = a9 ) by POLYNOM7:23; then A3: a9 | (n,L) = Monom (a9,(EmptyBag n)) by POLYNOM7:11; ( term (a | (n,L)) = EmptyBag n & coefficient (a | (n,L)) = a ) by POLYNOM7:23; then A4: a | (n,L) = Monom (a,(EmptyBag n)) by POLYNOM7:11; (EmptyBag n) + (EmptyBag n) = EmptyBag n by PRE_POLY:53; hence (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L)) by A1, A2, A4, A3, Th3; ::_thesis: verum end; supposeA5: ( a is zero or a9 is zero ) ; ::_thesis: (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L)) now__::_thesis:_(_(_a_=_0._L_&_(a_*_a9)_|_(n,L)_=_(a_|_(n,L))_*'_(a9_|_(n,L))_)_or_(_a9_=_0._L_&_(a_*_a9)_|_(n,L)_=_(a_|_(n,L))_*'_(a9_|_(n,L))_)_) percases ( a = 0. L or a9 = 0. L ) by A5, STRUCT_0:def_12; caseA6: a = 0. L ; ::_thesis: (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L)) then a * a9 = 0. L by BINOM:1; then A7: (a * a9) | (n,L) = 0_ (n,L) by POLYNOM7:19; a | (n,L) = 0_ (n,L) by A6, POLYNOM7:19; hence (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L)) by A7, Th2; ::_thesis: verum end; caseA8: a9 = 0. L ; ::_thesis: (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L)) then a * a9 = 0. L by BINOM:2; then A9: (a * a9) | (n,L) = 0_ (n,L) by POLYNOM7:19; a9 | (n,L) = 0_ (n,L) by A8, POLYNOM7:19; hence (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L)) by A9, POLYNOM1:28; ::_thesis: verum end; end; end; hence (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L)) ; ::_thesis: verum end; end; end; begin Lm1: for n being Ordinal for T being TermOrder of n for b being set st b in field T holds b is bag of n proof let n be Ordinal; ::_thesis: for T being TermOrder of n for b being set st b in field T holds b is bag of n let T be TermOrder of n; ::_thesis: for b being set st b in field T holds b is bag of n let b be set ; ::_thesis: ( b in field T implies b is bag of n ) assume b in field T ; ::_thesis: b is bag of n then A1: b in (dom T) \/ (rng T) by RELAT_1:def_6; percases ( b in dom T or b in rng T ) by A1, XBOOLE_0:def_3; suppose b in dom T ; ::_thesis: b is bag of n then b is Element of Bags n ; hence b is bag of n ; ::_thesis: verum end; suppose b in rng T ; ::_thesis: b is bag of n then b is Element of Bags n ; hence b is bag of n ; ::_thesis: verum end; end; end; registration let n be Ordinal; cluster Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric connected transitive admissible for Element of K19(K20((Bags n),(Bags n))); existence ex b1 being TermOrder of n st ( b1 is admissible & b1 is connected ) proof set T = LexOrder n; take LexOrder n ; ::_thesis: ( LexOrder n is admissible & LexOrder n is connected ) now__::_thesis:_for_x,_y_being_set_st_x_in_field_(LexOrder_n)_&_y_in_field_(LexOrder_n)_&_x_<>_y_&_not_[x,y]_in_LexOrder_n_holds_ [y,x]_in_LexOrder_n let x, y be set ; ::_thesis: ( x in field (LexOrder n) & y in field (LexOrder n) & x <> y & not [x,y] in LexOrder n implies [y,x] in LexOrder n ) assume that A1: ( x in field (LexOrder n) & y in field (LexOrder n) ) and x <> y ; ::_thesis: ( [x,y] in LexOrder n or [y,x] in LexOrder n ) reconsider b1 = x, b2 = y as bag of n by A1, Lm1; ( b1 <=' b2 or b2 <=' b1 ) by PRE_POLY:45; hence ( [x,y] in LexOrder n or [y,x] in LexOrder n ) by PRE_POLY:def_14; ::_thesis: verum end; then LexOrder n is_connected_in field (LexOrder n) by RELAT_2:def_6; hence ( LexOrder n is admissible & LexOrder n is connected ) by RELAT_2:def_14; ::_thesis: verum end; end; registration let n be Nat; cluster total reflexive antisymmetric transitive admissible -> well_founded admissible for Element of K19(K20((Bags n),(Bags n))); coherence for b1 being admissible TermOrder of n holds b1 is well_founded proof let T be admissible TermOrder of n; ::_thesis: T is well_founded T is well-ordering by BAGORDER:34; hence T is well_founded by WELLORD1:def_4; ::_thesis: verum end; end; definition let n be Ordinal; let T be TermOrder of n; let b, b9 be bag of n; predb <= b9,T means :Def2: :: TERMORD:def 2 [b,b9] in T; end; :: deftheorem Def2 defines <= TERMORD:def_2_:_ for n being Ordinal for T being TermOrder of n for b, b9 being bag of n holds ( b <= b9,T iff [b,b9] in T ); definition let n be Ordinal; let T be TermOrder of n; let b, b9 be bag of n; predb < b9,T means :Def3: :: TERMORD:def 3 ( b <= b9,T & b <> b9 ); end; :: deftheorem Def3 defines < TERMORD:def_3_:_ for n being Ordinal for T being TermOrder of n for b, b9 being bag of n holds ( b < b9,T iff ( b <= b9,T & b <> b9 ) ); definition let n be Ordinal; let T be TermOrder of n; let b1, b2 be bag of n; func min (b1,b2,T) -> bag of n equals :Def4: :: TERMORD:def 4 b1 if b1 <= b2,T otherwise b2; correctness coherence ( ( b1 <= b2,T implies b1 is bag of n ) & ( not b1 <= b2,T implies b2 is bag of n ) ); consistency for b1 being bag of n holds verum; ; func max (b1,b2,T) -> bag of n equals :Def5: :: TERMORD:def 5 b1 if b2 <= b1,T otherwise b2; correctness coherence ( ( b2 <= b1,T implies b1 is bag of n ) & ( not b2 <= b1,T implies b2 is bag of n ) ); consistency for b1 being bag of n holds verum; ; end; :: deftheorem Def4 defines min TERMORD:def_4_:_ for n being Ordinal for T being TermOrder of n for b1, b2 being bag of n holds ( ( b1 <= b2,T implies min (b1,b2,T) = b1 ) & ( not b1 <= b2,T implies min (b1,b2,T) = b2 ) ); :: deftheorem Def5 defines max TERMORD:def_5_:_ for n being Ordinal for T being TermOrder of n for b1, b2 being bag of n holds ( ( b2 <= b1,T implies max (b1,b2,T) = b1 ) & ( not b2 <= b1,T implies max (b1,b2,T) = b2 ) ); Lm2: for n being Ordinal for T being TermOrder of n for b being bag of n holds b <= b,T proof let n be Ordinal; ::_thesis: for T being TermOrder of n for b being bag of n holds b <= b,T let T be TermOrder of n; ::_thesis: for b being bag of n holds b <= b,T let b be bag of n; ::_thesis: b <= b,T field T = Bags n by ORDERS_1:12; then A1: T is_reflexive_in Bags n by RELAT_2:def_9; b is Element of Bags n by PRE_POLY:def_12; then [b,b] in T by A1, RELAT_2:def_1; hence b <= b,T by Def2; ::_thesis: verum end; Lm3: for n being Ordinal for T being TermOrder of n for b1, b2 being bag of n st b1 <= b2,T & b2 <= b1,T holds b1 = b2 proof let n be Ordinal; ::_thesis: for T being TermOrder of n for b1, b2 being bag of n st b1 <= b2,T & b2 <= b1,T holds b1 = b2 let T be TermOrder of n; ::_thesis: for b1, b2 being bag of n st b1 <= b2,T & b2 <= b1,T holds b1 = b2 let b1, b2 be bag of n; ::_thesis: ( b1 <= b2,T & b2 <= b1,T implies b1 = b2 ) field T = Bags n by ORDERS_1:12; then A1: T is_antisymmetric_in Bags n by RELAT_2:def_12; assume ( b1 <= b2,T & b2 <= b1,T ) ; ::_thesis: b1 = b2 then A2: ( [b1,b2] in T & [b2,b1] in T ) by Def2; ( b1 is Element of Bags n & b2 is Element of Bags n ) by PRE_POLY:def_12; hence b1 = b2 by A2, A1, RELAT_2:def_4; ::_thesis: verum end; Lm4: for n being Ordinal for T being TermOrder of n for b being bag of n holds b in field T proof let n be Ordinal; ::_thesis: for T being TermOrder of n for b being bag of n holds b in field T let T be TermOrder of n; ::_thesis: for b being bag of n holds b in field T let b be bag of n; ::_thesis: b in field T field T = Bags n by ORDERS_1:12; then A1: T is_reflexive_in Bags n by RELAT_2:def_9; b is Element of Bags n by PRE_POLY:def_12; then [b,b] in T by A1, RELAT_2:def_1; hence b in field T by RELAT_1:15; ::_thesis: verum end; theorem Th5: :: TERMORD:5 for n being Ordinal for T being connected TermOrder of n for b1, b2 being bag of n holds ( b1 <= b2,T iff not b2 < b1,T ) proof let n be Ordinal; ::_thesis: for T being connected TermOrder of n for b1, b2 being bag of n holds ( b1 <= b2,T iff not b2 < b1,T ) let T be connected TermOrder of n; ::_thesis: for b1, b2 being bag of n holds ( b1 <= b2,T iff not b2 < b1,T ) let b1, b2 be bag of n; ::_thesis: ( b1 <= b2,T iff not b2 < b1,T ) A1: T is_connected_in field T by RELAT_2:def_14; percases ( b1 = b2 or b1 <> b2 ) ; suppose b1 = b2 ; ::_thesis: ( b1 <= b2,T iff not b2 < b1,T ) hence ( b1 <= b2,T iff not b2 < b1,T ) by Def3, Lm2; ::_thesis: verum end; supposeA2: b1 <> b2 ; ::_thesis: ( b1 <= b2,T iff not b2 < b1,T ) A3: ( not b2 < b1,T implies b1 <= b2,T ) proof assume A4: not b2 < b1,T ; ::_thesis: b1 <= b2,T now__::_thesis:_(_(_not_b2_<=_b1,T_&_b1_<=_b2,T_)_or_(_b1_=_b2_&_b1_<=_b2,T_)_) percases ( not b2 <= b1,T or b1 = b2 ) by A4, Def3; caseA5: not b2 <= b1,T ; ::_thesis: b1 <= b2,T A6: ( b1 in field T & b2 in field T ) by Lm4; not [b2,b1] in T by A5, Def2; then [b1,b2] in T by A1, A2, A6, RELAT_2:def_6; hence b1 <= b2,T by Def2; ::_thesis: verum end; case b1 = b2 ; ::_thesis: b1 <= b2,T hence b1 <= b2,T by A2; ::_thesis: verum end; end; end; hence b1 <= b2,T ; ::_thesis: verum end; ( b1 <= b2,T implies not b2 < b1,T ) proof assume A7: b1 <= b2,T ; ::_thesis: not b2 < b1,T assume b2 < b1,T ; ::_thesis: contradiction then ( b2 <= b1,T & b1 <> b2 ) by Def3; hence contradiction by A7, Lm3; ::_thesis: verum end; hence ( b1 <= b2,T iff not b2 < b1,T ) by A3; ::_thesis: verum end; end; end; Lm5: for n being Ordinal for T being connected TermOrder of n for b1, b2 being bag of n holds ( b1 <= b2,T or b2 <= b1,T ) proof let n be Ordinal; ::_thesis: for T being connected TermOrder of n for b1, b2 being bag of n holds ( b1 <= b2,T or b2 <= b1,T ) let T be connected TermOrder of n; ::_thesis: for b1, b2 being bag of n holds ( b1 <= b2,T or b2 <= b1,T ) let b1, b2 be bag of n; ::_thesis: ( b1 <= b2,T or b2 <= b1,T ) A1: T is_connected_in field T by RELAT_2:def_14; percases ( b1 = b2 or b1 <> b2 ) ; supposeA2: b1 = b2 ; ::_thesis: ( b1 <= b2,T or b2 <= b1,T ) field T = Bags n by ORDERS_1:12; then A3: T is_reflexive_in Bags n by RELAT_2:def_9; b1 is Element of Bags n by PRE_POLY:def_12; then [b1,b2] in T by A2, A3, RELAT_2:def_1; hence ( b1 <= b2,T or b2 <= b1,T ) by Def2; ::_thesis: verum end; supposeA4: b1 <> b2 ; ::_thesis: ( b1 <= b2,T or b2 <= b1,T ) assume not b1 <= b2,T ; ::_thesis: b2 <= b1,T then A5: not [b1,b2] in T by Def2; ( b1 in field T & b2 in field T ) by Lm4; then [b2,b1] in T by A1, A4, A5, RELAT_2:def_6; hence b2 <= b1,T by Def2; ::_thesis: verum end; end; end; theorem :: TERMORD:6 for n being Ordinal for T being TermOrder of n for b being bag of n holds b <= b,T by Lm2; theorem :: TERMORD:7 for n being Ordinal for T being TermOrder of n for b1, b2 being bag of n st b1 <= b2,T & b2 <= b1,T holds b1 = b2 by Lm3; theorem Th8: :: TERMORD:8 for n being Ordinal for T being TermOrder of n for b1, b2, b3 being bag of n st b1 <= b2,T & b2 <= b3,T holds b1 <= b3,T proof let n be Ordinal; ::_thesis: for T being TermOrder of n for b1, b2, b3 being bag of n st b1 <= b2,T & b2 <= b3,T holds b1 <= b3,T let T be TermOrder of n; ::_thesis: for b1, b2, b3 being bag of n st b1 <= b2,T & b2 <= b3,T holds b1 <= b3,T let b1, b2, b3 be bag of n; ::_thesis: ( b1 <= b2,T & b2 <= b3,T implies b1 <= b3,T ) A1: b3 is Element of Bags n by PRE_POLY:def_12; field T = Bags n by ORDERS_1:12; then A2: T is_transitive_in Bags n by RELAT_2:def_16; assume ( b1 <= b2,T & b2 <= b3,T ) ; ::_thesis: b1 <= b3,T then A3: ( [b1,b2] in T & [b2,b3] in T ) by Def2; ( b1 is Element of Bags n & b2 is Element of Bags n ) by PRE_POLY:def_12; then [b1,b3] in T by A3, A2, A1, RELAT_2:def_8; hence b1 <= b3,T by Def2; ::_thesis: verum end; theorem Th9: :: TERMORD:9 for n being Ordinal for T being admissible TermOrder of n for b being bag of n holds EmptyBag n <= b,T proof let n be Ordinal; ::_thesis: for T being admissible TermOrder of n for b being bag of n holds EmptyBag n <= b,T let T be admissible TermOrder of n; ::_thesis: for b being bag of n holds EmptyBag n <= b,T let b be bag of n; ::_thesis: EmptyBag n <= b,T [(EmptyBag n),b] in T by BAGORDER:def_5; hence EmptyBag n <= b,T by Def2; ::_thesis: verum end; theorem :: TERMORD:10 for n being Ordinal for T being admissible TermOrder of n for b1, b2 being bag of n st b1 divides b2 holds b1 <= b2,T proof let n be Ordinal; ::_thesis: for T being admissible TermOrder of n for b1, b2 being bag of n st b1 divides b2 holds b1 <= b2,T let T be admissible TermOrder of n; ::_thesis: for b1, b2 being bag of n st b1 divides b2 holds b1 <= b2,T let b1, b2 be bag of n; ::_thesis: ( b1 divides b2 implies b1 <= b2,T ) assume b1 divides b2 ; ::_thesis: b1 <= b2,T then consider b3 being bag of n such that A1: b2 = b1 + b3 by Th1; EmptyBag n <= b3,T by Th9; then [(EmptyBag n),b3] in T by Def2; then [((EmptyBag n) + b1),b2] in T by A1, BAGORDER:def_5; then [b1,b2] in T by PRE_POLY:53; hence b1 <= b2,T by Def2; ::_thesis: verum end; theorem Th11: :: TERMORD:11 for n being Ordinal for T being TermOrder of n for b1, b2 being bag of n holds ( min (b1,b2,T) = b1 or min (b1,b2,T) = b2 ) proof let n be Ordinal; ::_thesis: for T being TermOrder of n for b1, b2 being bag of n holds ( min (b1,b2,T) = b1 or min (b1,b2,T) = b2 ) let T be TermOrder of n; ::_thesis: for b1, b2 being bag of n holds ( min (b1,b2,T) = b1 or min (b1,b2,T) = b2 ) let b1, b2 be bag of n; ::_thesis: ( min (b1,b2,T) = b1 or min (b1,b2,T) = b2 ) assume A1: min (b1,b2,T) <> b1 ; ::_thesis: min (b1,b2,T) = b2 now__::_thesis:_(_(_not_b1_<=_b2,T_&_min_(b1,b2,T)_=_b2_)_or_(_b1_=_b2_&_contradiction_)_) percases ( not b1 <= b2,T or b1 = b2 ) by A1, Def4; case not b1 <= b2,T ; ::_thesis: min (b1,b2,T) = b2 hence min (b1,b2,T) = b2 by Def4; ::_thesis: verum end; case b1 = b2 ; ::_thesis: contradiction then b1 <= b2,T by Lm2; hence contradiction by A1, Def4; ::_thesis: verum end; end; end; hence min (b1,b2,T) = b2 ; ::_thesis: verum end; theorem Th12: :: TERMORD:12 for n being Ordinal for T being TermOrder of n for b1, b2 being bag of n holds ( max (b1,b2,T) = b1 or max (b1,b2,T) = b2 ) proof let n be Ordinal; ::_thesis: for T being TermOrder of n for b1, b2 being bag of n holds ( max (b1,b2,T) = b1 or max (b1,b2,T) = b2 ) let T be TermOrder of n; ::_thesis: for b1, b2 being bag of n holds ( max (b1,b2,T) = b1 or max (b1,b2,T) = b2 ) let b1, b2 be bag of n; ::_thesis: ( max (b1,b2,T) = b1 or max (b1,b2,T) = b2 ) assume A1: max (b1,b2,T) <> b1 ; ::_thesis: max (b1,b2,T) = b2 now__::_thesis:_(_(_not_b2_<=_b1,T_&_max_(b1,b2,T)_=_b2_)_or_(_b1_=_b2_&_contradiction_)_) percases ( not b2 <= b1,T or b1 = b2 ) by A1, Def5; case not b2 <= b1,T ; ::_thesis: max (b1,b2,T) = b2 hence max (b1,b2,T) = b2 by Def5; ::_thesis: verum end; case b1 = b2 ; ::_thesis: contradiction then b2 <= b1,T by Lm2; hence contradiction by A1, Def5; ::_thesis: verum end; end; end; hence max (b1,b2,T) = b2 ; ::_thesis: verum end; Lm6: for n being Ordinal for T being TermOrder of n for b being bag of n holds ( min (b,b,T) = b & max (b,b,T) = b ) proof let n be Ordinal; ::_thesis: for T being TermOrder of n for b being bag of n holds ( min (b,b,T) = b & max (b,b,T) = b ) let T be TermOrder of n; ::_thesis: for b being bag of n holds ( min (b,b,T) = b & max (b,b,T) = b ) let b be bag of n; ::_thesis: ( min (b,b,T) = b & max (b,b,T) = b ) thus min (b,b,T) = b by Def4; ::_thesis: max (b,b,T) = b thus max (b,b,T) = b by Def5; ::_thesis: verum end; theorem :: TERMORD:13 for n being Ordinal for T being connected TermOrder of n for b1, b2 being bag of n holds ( min (b1,b2,T) <= b1,T & min (b1,b2,T) <= b2,T ) proof let n be Ordinal; ::_thesis: for T being connected TermOrder of n for b1, b2 being bag of n holds ( min (b1,b2,T) <= b1,T & min (b1,b2,T) <= b2,T ) let T be connected TermOrder of n; ::_thesis: for b1, b2 being bag of n holds ( min (b1,b2,T) <= b1,T & min (b1,b2,T) <= b2,T ) let b1, b2 be bag of n; ::_thesis: ( min (b1,b2,T) <= b1,T & min (b1,b2,T) <= b2,T ) percases ( b1 <= b2,T or b2 <= b1,T ) by Lm5; supposeA1: b1 <= b2,T ; ::_thesis: ( min (b1,b2,T) <= b1,T & min (b1,b2,T) <= b2,T ) then min (b1,b2,T) = b1 by Def4; hence ( min (b1,b2,T) <= b1,T & min (b1,b2,T) <= b2,T ) by A1, Lm2; ::_thesis: verum end; supposeA2: b2 <= b1,T ; ::_thesis: ( min (b1,b2,T) <= b1,T & min (b1,b2,T) <= b2,T ) now__::_thesis:_(_(_b1_=_b2_&_min_(b1,b2,T)_<=_b1,T_&_min_(b1,b2,T)_<=_b2,T_)_or_(_b1_<>_b2_&_min_(b1,b2,T)_<=_b1,T_&_min_(b1,b2,T)_<=_b2,T_)_) percases ( b1 = b2 or b1 <> b2 ) ; caseA3: b1 = b2 ; ::_thesis: ( min (b1,b2,T) <= b1,T & min (b1,b2,T) <= b2,T ) then min (b1,b2,T) = b1 by Lm6; hence ( min (b1,b2,T) <= b1,T & min (b1,b2,T) <= b2,T ) by A3, Lm2; ::_thesis: verum end; case b1 <> b2 ; ::_thesis: ( min (b1,b2,T) <= b1,T & min (b1,b2,T) <= b2,T ) then b2 < b1,T by A2, Def3; then not b1 <= b2,T by Th5; then min (b1,b2,T) = b2 by Def4; hence ( min (b1,b2,T) <= b1,T & min (b1,b2,T) <= b2,T ) by A2, Lm2; ::_thesis: verum end; end; end; hence ( min (b1,b2,T) <= b1,T & min (b1,b2,T) <= b2,T ) ; ::_thesis: verum end; end; end; theorem Th14: :: TERMORD:14 for n being Ordinal for T being connected TermOrder of n for b1, b2 being bag of n holds ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T ) proof let n be Ordinal; ::_thesis: for T being connected TermOrder of n for b1, b2 being bag of n holds ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T ) let T be connected TermOrder of n; ::_thesis: for b1, b2 being bag of n holds ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T ) let b1, b2 be bag of n; ::_thesis: ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T ) percases ( b2 <= b1,T or b1 <= b2,T ) by Lm5; supposeA1: b2 <= b1,T ; ::_thesis: ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T ) then max (b1,b2,T) = b1 by Def5; hence ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T ) by A1, Lm2; ::_thesis: verum end; supposeA2: b1 <= b2,T ; ::_thesis: ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T ) now__::_thesis:_(_(_b1_=_b2_&_b1_<=_max_(b1,b2,T),T_&_b2_<=_max_(b1,b2,T),T_)_or_(_b1_<>_b2_&_b1_<=_max_(b1,b2,T),T_&_b2_<=_max_(b1,b2,T),T_)_) percases ( b1 = b2 or b1 <> b2 ) ; caseA3: b1 = b2 ; ::_thesis: ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T ) then max (b1,b2,T) = b1 by Lm6; hence ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T ) by A3, Lm2; ::_thesis: verum end; case b1 <> b2 ; ::_thesis: ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T ) then b1 < b2,T by A2, Def3; then not b2 <= b1,T by Th5; then max (b1,b2,T) = b2 by Def5; hence ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T ) by A2, Lm2; ::_thesis: verum end; end; end; hence ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T ) ; ::_thesis: verum end; end; end; theorem Th15: :: TERMORD:15 for n being Ordinal for T being connected TermOrder of n for b1, b2 being bag of n holds ( min (b1,b2,T) = min (b2,b1,T) & max (b1,b2,T) = max (b2,b1,T) ) proof let n be Ordinal; ::_thesis: for T being connected TermOrder of n for b1, b2 being bag of n holds ( min (b1,b2,T) = min (b2,b1,T) & max (b1,b2,T) = max (b2,b1,T) ) let T be connected TermOrder of n; ::_thesis: for b1, b2 being bag of n holds ( min (b1,b2,T) = min (b2,b1,T) & max (b1,b2,T) = max (b2,b1,T) ) let b1, b2 be bag of n; ::_thesis: ( min (b1,b2,T) = min (b2,b1,T) & max (b1,b2,T) = max (b2,b1,T) ) now__::_thesis:_(_(_min_(b1,b2,T)_=_b1_&_min_(b1,b2,T)_=_min_(b2,b1,T)_)_or_(_min_(b1,b2,T)_<>_b1_&_min_(b1,b2,T)_=_min_(b2,b1,T)_)_) percases ( min (b1,b2,T) = b1 or min (b1,b2,T) <> b1 ) ; caseA1: min (b1,b2,T) = b1 ; ::_thesis: min (b1,b2,T) = min (b2,b1,T) now__::_thesis:_(_(_b1_<=_b2,T_&_min_(b1,b2,T)_=_min_(b2,b1,T)_)_or_(_b1_=_b2_&_min_(b2,b1,T)_=_min_(b1,b2,T)_)_) percases ( b1 <= b2,T or b1 = b2 ) by A1, Def4; caseA2: b1 <= b2,T ; ::_thesis: min (b1,b2,T) = min (b2,b1,T) now__::_thesis:_(_(_b1_=_b2_&_min_(b2,b1,T)_=_min_(b1,b2,T)_)_or_(_b1_<>_b2_&_min_(b2,b1,T)_=_min_(b1,b2,T)_)_) percases ( b1 = b2 or b1 <> b2 ) ; case b1 = b2 ; ::_thesis: min (b2,b1,T) = min (b1,b2,T) hence min (b2,b1,T) = min (b1,b2,T) ; ::_thesis: verum end; case b1 <> b2 ; ::_thesis: min (b2,b1,T) = min (b1,b2,T) then not b2 <= b1,T by A2, Lm3; hence min (b2,b1,T) = min (b1,b2,T) by A1, Def4; ::_thesis: verum end; end; end; hence min (b1,b2,T) = min (b2,b1,T) ; ::_thesis: verum end; case b1 = b2 ; ::_thesis: min (b2,b1,T) = min (b1,b2,T) hence min (b2,b1,T) = min (b1,b2,T) ; ::_thesis: verum end; end; end; hence min (b1,b2,T) = min (b2,b1,T) ; ::_thesis: verum end; caseA3: min (b1,b2,T) <> b1 ; ::_thesis: min (b1,b2,T) = min (b2,b1,T) A4: now__::_thesis:_b2_<=_b1,T assume not b2 <= b1,T ; ::_thesis: contradiction then b1 <= b2,T by Lm5; hence contradiction by A3, Def4; ::_thesis: verum end; thus min (b1,b2,T) = b2 by A3, Th11 .= min (b2,b1,T) by A4, Def4 ; ::_thesis: verum end; end; end; hence min (b1,b2,T) = min (b2,b1,T) ; ::_thesis: max (b1,b2,T) = max (b2,b1,T) now__::_thesis:_(_(_max_(b1,b2,T)_=_b1_&_max_(b1,b2,T)_=_max_(b2,b1,T)_)_or_(_max_(b1,b2,T)_<>_b1_&_max_(b2,b1,T)_=_max_(b1,b2,T)_)_) percases ( max (b1,b2,T) = b1 or max (b1,b2,T) <> b1 ) ; caseA5: max (b1,b2,T) = b1 ; ::_thesis: max (b1,b2,T) = max (b2,b1,T) now__::_thesis:_(_(_b2_<=_b1,T_&_max_(b1,b2,T)_=_max_(b2,b1,T)_)_or_(_b1_=_b2_&_max_(b2,b1,T)_=_max_(b1,b2,T)_)_) percases ( b2 <= b1,T or b1 = b2 ) by A5, Def5; caseA6: b2 <= b1,T ; ::_thesis: max (b1,b2,T) = max (b2,b1,T) now__::_thesis:_(_(_b1_=_b2_&_max_(b2,b1,T)_=_max_(b1,b2,T)_)_or_(_b1_<>_b2_&_max_(b2,b1,T)_=_max_(b1,b2,T)_)_) percases ( b1 = b2 or b1 <> b2 ) ; case b1 = b2 ; ::_thesis: max (b2,b1,T) = max (b1,b2,T) hence max (b2,b1,T) = max (b1,b2,T) ; ::_thesis: verum end; case b1 <> b2 ; ::_thesis: max (b2,b1,T) = max (b1,b2,T) then not b1 <= b2,T by A6, Lm3; hence max (b2,b1,T) = max (b1,b2,T) by A5, Def5; ::_thesis: verum end; end; end; hence max (b1,b2,T) = max (b2,b1,T) ; ::_thesis: verum end; case b1 = b2 ; ::_thesis: max (b2,b1,T) = max (b1,b2,T) hence max (b2,b1,T) = max (b1,b2,T) ; ::_thesis: verum end; end; end; hence max (b1,b2,T) = max (b2,b1,T) ; ::_thesis: verum end; caseA7: max (b1,b2,T) <> b1 ; ::_thesis: max (b2,b1,T) = max (b1,b2,T) now__::_thesis:_(_(_b1_<=_b2,T_&_max_(b2,b1,T)_=_max_(b1,b2,T)_)_or_(_b2_<=_b1,T_&_max_(b2,b1,T)_=_max_(b1,b2,T)_)_) percases ( b1 <= b2,T or b2 <= b1,T ) by Lm5; case b1 <= b2,T ; ::_thesis: max (b2,b1,T) = max (b1,b2,T) hence max (b2,b1,T) = b2 by Def5 .= max (b1,b2,T) by A7, Th12 ; ::_thesis: verum end; case b2 <= b1,T ; ::_thesis: max (b2,b1,T) = max (b1,b2,T) hence max (b2,b1,T) = max (b1,b2,T) by A7, Def5; ::_thesis: verum end; end; end; hence max (b2,b1,T) = max (b1,b2,T) ; ::_thesis: verum end; end; end; hence max (b1,b2,T) = max (b2,b1,T) ; ::_thesis: verum end; theorem :: TERMORD:16 for n being Ordinal for T being connected TermOrder of n for b1, b2 being bag of n holds ( min (b1,b2,T) = b1 iff max (b1,b2,T) = b2 ) proof let n be Ordinal; ::_thesis: for T being connected TermOrder of n for b1, b2 being bag of n holds ( min (b1,b2,T) = b1 iff max (b1,b2,T) = b2 ) let T be connected TermOrder of n; ::_thesis: for b1, b2 being bag of n holds ( min (b1,b2,T) = b1 iff max (b1,b2,T) = b2 ) let b1, b2 be bag of n; ::_thesis: ( min (b1,b2,T) = b1 iff max (b1,b2,T) = b2 ) A1: now__::_thesis:_(_max_(b1,b2,T)_=_b2_implies_min_(b1,b2,T)_=_b1_) assume A2: max (b1,b2,T) = b2 ; ::_thesis: min (b1,b2,T) = b1 now__::_thesis:_(_(_not_b2_<=_b1,T_&_min_(b1,b2,T)_=_b1_)_or_(_b1_=_b2_&_min_(b1,b2,T)_=_b1_)_) percases ( not b2 <= b1,T or b1 = b2 ) by A2, Def5; case not b2 <= b1,T ; ::_thesis: min (b1,b2,T) = b1 then b1 <= b2,T by Lm5; hence min (b1,b2,T) = b1 by Def4; ::_thesis: verum end; case b1 = b2 ; ::_thesis: min (b1,b2,T) = b1 hence min (b1,b2,T) = b1 by Th11; ::_thesis: verum end; end; end; hence min (b1,b2,T) = b1 ; ::_thesis: verum end; now__::_thesis:_(_min_(b1,b2,T)_=_b1_implies_max_(b1,b2,T)_=_b2_) assume A3: min (b1,b2,T) = b1 ; ::_thesis: max (b1,b2,T) = b2 now__::_thesis:_(_(_b1_<=_b2,T_&_max_(b1,b2,T)_=_b2_)_or_(_b1_=_b2_&_max_(b1,b2,T)_=_b2_)_) percases ( b1 <= b2,T or b1 = b2 ) by A3, Def4; case b1 <= b2,T ; ::_thesis: max (b1,b2,T) = b2 then max (b2,b1,T) = b2 by Def5; hence max (b1,b2,T) = b2 by Th15; ::_thesis: verum end; case b1 = b2 ; ::_thesis: max (b1,b2,T) = b2 hence max (b1,b2,T) = b2 by Th12; ::_thesis: verum end; end; end; hence max (b1,b2,T) = b2 ; ::_thesis: verum end; hence ( min (b1,b2,T) = b1 iff max (b1,b2,T) = b2 ) by A1; ::_thesis: verum end; begin definition let n be Ordinal; let T be connected TermOrder of n; let L be non empty ZeroStr ; let p be Polynomial of n,L; func HT (p,T) -> Element of Bags n means :Def6: :: TERMORD:def 6 ( ( Support p = {} & it = EmptyBag n ) or ( it in Support p & ( for b being bag of n st b in Support p holds b <= it,T ) ) ); existence ex b1 being Element of Bags n st ( ( Support p = {} & b1 = EmptyBag n ) or ( b1 in Support p & ( for b being bag of n st b in Support p holds b <= b1,T ) ) ) proof set O = T; percases ( Support p = {} or Support p <> {} ) ; suppose Support p = {} ; ::_thesis: ex b1 being Element of Bags n st ( ( Support p = {} & b1 = EmptyBag n ) or ( b1 in Support p & ( for b being bag of n st b in Support p holds b <= b1,T ) ) ) hence ex b1 being Element of Bags n st ( ( Support p = {} & b1 = EmptyBag n ) or ( b1 in Support p & ( for b being bag of n st b in Support p holds b <= b1,T ) ) ) ; ::_thesis: verum end; supposeA1: Support p <> {} ; ::_thesis: ex b1 being Element of Bags n st ( ( Support p = {} & b1 = EmptyBag n ) or ( b1 in Support p & ( for b being bag of n st b in Support p holds b <= b1,T ) ) ) reconsider sp = Support p as finite set by POLYNOM1:def_4; card sp is finite ; then consider m being Nat such that A2: card (Support p) = card m by CARD_1:48; reconsider sp = Support p as finite Subset of (Bags n) by POLYNOM1:def_4; defpred S1[ Nat] means for B being finite Subset of (Bags n) st card B = $1 holds ex b9 being bag of n st ( b9 in B & ( for b being bag of n st b in B holds [b,b9] in T ) ); A3: for k being Nat st 1 <= k & S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( 1 <= k & S1[k] implies S1[k + 1] ) assume A4: 1 <= k ; ::_thesis: ( not S1[k] or S1[k + 1] ) thus ( S1[k] implies S1[k + 1] ) ::_thesis: verum proof assume A5: S1[k] ; ::_thesis: S1[k + 1] thus S1[k + 1] ::_thesis: verum proof let B be finite Subset of (Bags n); ::_thesis: ( card B = k + 1 implies ex b9 being bag of n st ( b9 in B & ( for b being bag of n st b in B holds [b,b9] in T ) ) ) assume A6: card B = k + 1 ; ::_thesis: ex b9 being bag of n st ( b9 in B & ( for b being bag of n st b in B holds [b,b9] in T ) ) then reconsider B = B as non empty finite Subset of (Bags n) ; set x = the Element of B; reconsider x = the Element of B as Element of Bags n ; reconsider x = x as bag of n ; set X = B \ {x}; now__::_thesis:_for_u_being_set_st_u_in_{x}_holds_ u_in_B let u be set ; ::_thesis: ( u in {x} implies u in B ) assume u in {x} ; ::_thesis: u in B then u = x by TARSKI:def_1; hence u in B ; ::_thesis: verum end; then {x} c= B by TARSKI:def_3; then A7: B = {x} \/ B by XBOOLE_1:12 .= {x} \/ (B \ {x}) by XBOOLE_1:39 ; ( x in B \ {x} iff ( x in B & not x in {x} ) ) by XBOOLE_0:def_5; then A8: (card (B \ {x})) + 1 = k + 1 by A6, A7, CARD_2:41, TARSKI:def_1; then reconsider X = B \ {x} as non empty set by A4; consider b9 being bag of n such that A9: b9 in X and A10: for b being bag of n st b in X holds [b,b9] in T by A5, A8; A11: T is_connected_in field T by RELAT_2:def_14; now__::_thesis:_(_(_x_=_b9_&_ex_b9,_b9_being_bag_of_n_st_ (_b9_in_B_&_(_for_b_being_bag_of_n_st_b_in_B_holds_ [b,b9]_in_T_)_)_)_or_(_x_<>_b9_&_ex_b9_being_bag_of_n_st_ (_b9_in_B_&_(_for_b_being_bag_of_n_st_b_in_B_holds_ [b,b9]_in_T_)_)_)_) percases ( x = b9 or x <> b9 ) ; caseA12: x = b9 ; ::_thesis: ex b9, b9 being bag of n st ( b9 in B & ( for b being bag of n st b in B holds [b,b9] in T ) ) A13: now__::_thesis:_for_b_being_bag_of_n_st_b_in_B_holds_ [b,b9]_in_T let b be bag of n; ::_thesis: ( b in B implies [b,b9] in T ) assume A14: b in B ; ::_thesis: [b,b9] in T now__::_thesis:_(_(_b_in_X_&_[b,b9]_in_T_)_or_(_not_b_in_X_&_[b,b9]_in_T_)_) percases ( b in X or not b in X ) ; case b in X ; ::_thesis: [b,b9] in T hence [b,b9] in T by A10; ::_thesis: verum end; case not b in X ; ::_thesis: [b,b9] in T then b in {x} by A7, A14, XBOOLE_0:def_3; then b = x by TARSKI:def_1; hence [b,b9] in T by A12, ORDERS_1:3; ::_thesis: verum end; end; end; hence [b,b9] in T ; ::_thesis: verum end; take b9 = b9; ::_thesis: ex b9 being bag of n st ( b9 in B & ( for b being bag of n st b in B holds [b,b9] in T ) ) X c= B by XBOOLE_1:36; hence ex b9 being bag of n st ( b9 in B & ( for b being bag of n st b in B holds [b,b9] in T ) ) by A9, A13; ::_thesis: verum end; caseA15: x <> b9 ; ::_thesis: ex b9 being bag of n st ( b9 in B & ( for b being bag of n st b in B holds [b,b9] in T ) ) b9 is Element of Bags n by PRE_POLY:def_12; then [b9,b9] in T by ORDERS_1:3; then A16: b9 in field T by RELAT_1:15; [x,x] in T by ORDERS_1:3; then A17: x in field T by RELAT_1:15; now__::_thesis:_(_(_[x,b9]_in_T_&_ex_b9_being_bag_of_n_st_ (_b9_in_B_&_(_for_b_being_bag_of_n_st_b_in_B_holds_ [b,b9]_in_T_)_)_)_or_(_[b9,x]_in_T_&_ex_b9_being_bag_of_n_st_ (_b9_in_B_&_(_for_b_being_bag_of_n_st_b_in_B_holds_ [b,b9]_in_T_)_)_)_) percases ( [x,b9] in T or [b9,x] in T ) by A11, A15, A17, A16, RELAT_2:def_6; caseA18: [x,b9] in T ; ::_thesis: ex b9 being bag of n st ( b9 in B & ( for b being bag of n st b in B holds [b,b9] in T ) ) thus ex b9 being bag of n st ( b9 in B & ( for b being bag of n st b in B holds [b,b9] in T ) ) ::_thesis: verum proof take b9 ; ::_thesis: ( b9 in B & ( for b being bag of n st b in B holds [b,b9] in T ) ) for b being bag of n st b in B holds [b,b9] in T proof let b be bag of n; ::_thesis: ( b in B implies [b,b9] in T ) assume A19: b in B ; ::_thesis: [b,b9] in T now__::_thesis:_(_(_b_<>_x_&_[b,b9]_in_T_)_or_(_b_=_x_&_[b,b9]_in_T_)_) percases ( b <> x or b = x ) ; case b <> x ; ::_thesis: [b,b9] in T then not b in {x} by TARSKI:def_1; then b in X by A19, XBOOLE_0:def_5; hence [b,b9] in T by A10; ::_thesis: verum end; case b = x ; ::_thesis: [b,b9] in T hence [b,b9] in T by A18; ::_thesis: verum end; end; end; hence [b,b9] in T ; ::_thesis: verum end; hence ( b9 in B & ( for b being bag of n st b in B holds [b,b9] in T ) ) by A9, XBOOLE_0:def_5; ::_thesis: verum end; end; caseA20: [b9,x] in T ; ::_thesis: ex b9 being bag of n st ( b9 in B & ( for b being bag of n st b in B holds [b,b9] in T ) ) thus ex b9 being bag of n st ( b9 in B & ( for b being bag of n st b in B holds [b,b9] in T ) ) ::_thesis: verum proof take x ; ::_thesis: ( x in B & ( for b being bag of n st b in B holds [b,x] in T ) ) for b being bag of n st b in B holds [b,x] in T proof let b be bag of n; ::_thesis: ( b in B implies [b,x] in T ) assume A21: b in B ; ::_thesis: [b,x] in T now__::_thesis:_(_(_b_<>_x_&_[b,x]_in_T_)_or_(_b_=_x_&_[b,x]_in_T_)_) percases ( b <> x or b = x ) ; case b <> x ; ::_thesis: [b,x] in T then not b in {x} by TARSKI:def_1; then b in X by A21, XBOOLE_0:def_5; then A22: [b,b9] in T by A10; ( b is Element of Bags n & b9 is Element of Bags n ) by PRE_POLY:def_12; hence [b,x] in T by A20, A22, ORDERS_1:5; ::_thesis: verum end; case b = x ; ::_thesis: [b,x] in T hence [b,x] in T by ORDERS_1:3; ::_thesis: verum end; end; end; hence [b,x] in T ; ::_thesis: verum end; hence ( x in B & ( for b being bag of n st b in B holds [b,x] in T ) ) ; ::_thesis: verum end; end; end; end; hence ex b9 being bag of n st ( b9 in B & ( for b being bag of n st b in B holds [b,b9] in T ) ) ; ::_thesis: verum end; end; end; hence ex b9 being bag of n st ( b9 in B & ( for b being bag of n st b in B holds [b,b9] in T ) ) ; ::_thesis: verum end; end; end; m <> 0 by A1, A2; then A23: 1 <= m by NAT_1:14; A24: card (Support p) = m by A2, CARD_1:def_2; A25: S1[1] proof let B be finite Subset of (Bags n); ::_thesis: ( card B = 1 implies ex b9 being bag of n st ( b9 in B & ( for b being bag of n st b in B holds [b,b9] in T ) ) ) assume card B = 1 ; ::_thesis: ex b9 being bag of n st ( b9 in B & ( for b being bag of n st b in B holds [b,b9] in T ) ) then card {{}} = card B by CARD_1:30; then consider b being set such that A26: B = {b} by CARD_1:29; A27: b in B by A26, TARSKI:def_1; then reconsider b = b as Element of Bags n ; reconsider b = b as bag of n ; now__::_thesis:_for_b9_being_bag_of_n_st_b9_in_B_holds_ [b9,b]_in_T let b9 be bag of n; ::_thesis: ( b9 in B implies [b9,b] in T ) assume b9 in B ; ::_thesis: [b9,b] in T then b9 = b by A26, TARSKI:def_1; hence [b9,b] in T by ORDERS_1:3; ::_thesis: verum end; hence ex b9 being bag of n st ( b9 in B & ( for b being bag of n st b in B holds [b,b9] in T ) ) by A27; ::_thesis: verum end; for k being Nat st 1 <= k holds S1[k] from NAT_1:sch_8(A25, A3); then consider b9 being bag of n such that A28: b9 in sp and A29: for b being bag of n st b in sp holds [b,b9] in T by A24, A23; take b9 ; ::_thesis: ( b9 is Element of Bags n & b9 is Element of Bags n & not ( not ( Support p = {} & b9 = EmptyBag n ) & not ( b9 in Support p & ( for b being bag of n st b in Support p holds b <= b9,T ) ) ) ) now__::_thesis:_for_b_being_bag_of_n_st_b_in_sp_holds_ b_<=_b9,T let b be bag of n; ::_thesis: ( b in sp implies b <= b9,T ) assume b in sp ; ::_thesis: b <= b9,T then [b,b9] in T by A29; hence b <= b9,T by Def2; ::_thesis: verum end; hence ( b9 is Element of Bags n & b9 is Element of Bags n & not ( not ( Support p = {} & b9 = EmptyBag n ) & not ( b9 in Support p & ( for b being bag of n st b in Support p holds b <= b9,T ) ) ) ) by A28; ::_thesis: verum end; end; end; uniqueness for b1, b2 being Element of Bags n st ( ( Support p = {} & b1 = EmptyBag n ) or ( b1 in Support p & ( for b being bag of n st b in Support p holds b <= b1,T ) ) ) & ( ( Support p = {} & b2 = EmptyBag n ) or ( b2 in Support p & ( for b being bag of n st b in Support p holds b <= b2,T ) ) ) holds b1 = b2 proof let b1, b2 be Element of Bags n; ::_thesis: ( ( ( Support p = {} & b1 = EmptyBag n ) or ( b1 in Support p & ( for b being bag of n st b in Support p holds b <= b1,T ) ) ) & ( ( Support p = {} & b2 = EmptyBag n ) or ( b2 in Support p & ( for b being bag of n st b in Support p holds b <= b2,T ) ) ) implies b1 = b2 ) set O = T; assume A30: ( ( Support p = {} & b1 = EmptyBag n ) or ( b1 in Support p & ( for b being bag of n st b in Support p holds b <= b1,T ) ) ) ; ::_thesis: ( ( not ( Support p = {} & b2 = EmptyBag n ) & not ( b2 in Support p & ( for b being bag of n st b in Support p holds b <= b2,T ) ) ) or b1 = b2 ) assume A31: ( ( Support p = {} & b2 = EmptyBag n ) or ( b2 in Support p & ( for b being bag of n st b in Support p holds b <= b2,T ) ) ) ; ::_thesis: b1 = b2 percases ( Support p = {} or Support p <> {} ) ; suppose Support p = {} ; ::_thesis: b1 = b2 hence b1 = b2 by A30, A31; ::_thesis: verum end; supposeA32: Support p <> {} ; ::_thesis: b1 = b2 then b1 <= b2,T by A30, A31; then A33: [b1,b2] in T by Def2; b2 <= b1,T by A30, A31, A32; then [b2,b1] in T by Def2; hence b1 = b2 by A33, ORDERS_1:4; ::_thesis: verum end; end; end; end; :: deftheorem Def6 defines HT TERMORD:def_6_:_ for n being Ordinal for T being connected TermOrder of n for L being non empty ZeroStr for p being Polynomial of n,L for b5 being Element of Bags n holds ( b5 = HT (p,T) iff ( ( Support p = {} & b5 = EmptyBag n ) or ( b5 in Support p & ( for b being bag of n st b in Support p holds b <= b5,T ) ) ) ); definition let n be Ordinal; let T be connected TermOrder of n; let L be non empty ZeroStr ; let p be Polynomial of n,L; func HC (p,T) -> Element of L equals :: TERMORD:def 7 p . (HT (p,T)); correctness coherence p . (HT (p,T)) is Element of L; ; end; :: deftheorem defines HC TERMORD:def_7_:_ for n being Ordinal for T being connected TermOrder of n for L being non empty ZeroStr for p being Polynomial of n,L holds HC (p,T) = p . (HT (p,T)); definition let n be Ordinal; let T be connected TermOrder of n; let L be non empty ZeroStr ; let p be Polynomial of n,L; func HM (p,T) -> Monomial of n,L equals :: TERMORD:def 8 Monom ((HC (p,T)),(HT (p,T))); correctness coherence Monom ((HC (p,T)),(HT (p,T))) is Monomial of n,L; ; end; :: deftheorem defines HM TERMORD:def_8_:_ for n being Ordinal for T being connected TermOrder of n for L being non empty ZeroStr for p being Polynomial of n,L holds HM (p,T) = Monom ((HC (p,T)),(HT (p,T))); Lm7: for n being Ordinal for O being connected TermOrder of n for L being non empty ZeroStr for p being Polynomial of n,L holds ( HC (p,O) = 0. L iff p = 0_ (n,L) ) proof let n be Ordinal; ::_thesis: for O being connected TermOrder of n for L being non empty ZeroStr for p being Polynomial of n,L holds ( HC (p,O) = 0. L iff p = 0_ (n,L) ) let O be connected TermOrder of n; ::_thesis: for L being non empty ZeroStr for p being Polynomial of n,L holds ( HC (p,O) = 0. L iff p = 0_ (n,L) ) let L be non empty ZeroStr ; ::_thesis: for p being Polynomial of n,L holds ( HC (p,O) = 0. L iff p = 0_ (n,L) ) let p be Polynomial of n,L; ::_thesis: ( HC (p,O) = 0. L iff p = 0_ (n,L) ) now__::_thesis:_(_HC_(p,O)_=_0._L_implies_p_=_0__(n,L)_) assume HC (p,O) = 0. L ; ::_thesis: p = 0_ (n,L) then not HT (p,O) in Support p by POLYNOM1:def_3; then Support p = {} by Def6; hence p = 0_ (n,L) by POLYNOM7:1; ::_thesis: verum end; hence ( HC (p,O) = 0. L iff p = 0_ (n,L) ) by POLYNOM1:22; ::_thesis: verum end; Lm8: for n being Ordinal for O being connected TermOrder of n for L being non trivial ZeroStr for p being Polynomial of n,L holds (HM (p,O)) . (HT (p,O)) = p . (HT (p,O)) proof let n be Ordinal; ::_thesis: for O being connected TermOrder of n for L being non trivial ZeroStr for p being Polynomial of n,L holds (HM (p,O)) . (HT (p,O)) = p . (HT (p,O)) let O be connected TermOrder of n; ::_thesis: for L being non trivial ZeroStr for p being Polynomial of n,L holds (HM (p,O)) . (HT (p,O)) = p . (HT (p,O)) let L be non trivial ZeroStr ; ::_thesis: for p being Polynomial of n,L holds (HM (p,O)) . (HT (p,O)) = p . (HT (p,O)) let p be Polynomial of n,L; ::_thesis: (HM (p,O)) . (HT (p,O)) = p . (HT (p,O)) A1: now__::_thesis:_(_(_HC_(p,O)_<>_0._L_&_term_(HM_(p,O))_=_HT_(p,O)_)_or_(_HC_(p,O)_=_0._L_&_term_(HM_(p,O))_=_HT_(p,O)_)_) percases ( HC (p,O) <> 0. L or HC (p,O) = 0. L ) ; case HC (p,O) <> 0. L ; ::_thesis: term (HM (p,O)) = HT (p,O) then not HC (p,O) is zero by STRUCT_0:def_12; hence term (HM (p,O)) = HT (p,O) by POLYNOM7:10; ::_thesis: verum end; caseA2: HC (p,O) = 0. L ; ::_thesis: term (HM (p,O)) = HT (p,O) then p = 0_ (n,L) by Lm7; then Support p = {} by POLYNOM7:1; then HT (p,O) = EmptyBag n by Def6; hence term (HM (p,O)) = HT (p,O) by A2, POLYNOM7:8; ::_thesis: verum end; end; end; p . (HT (p,O)) = coefficient (HM (p,O)) by POLYNOM7:9 .= (HM (p,O)) . (term (HM (p,O))) by POLYNOM7:def_6 ; hence (HM (p,O)) . (HT (p,O)) = p . (HT (p,O)) by A1; ::_thesis: verum end; Lm9: for n being Ordinal for O being connected TermOrder of n for L being non trivial ZeroStr for p being Polynomial of n,L st HC (p,O) <> 0. L holds HT (p,O) in Support (HM (p,O)) proof let n be Ordinal; ::_thesis: for O being connected TermOrder of n for L being non trivial ZeroStr for p being Polynomial of n,L st HC (p,O) <> 0. L holds HT (p,O) in Support (HM (p,O)) let O be connected TermOrder of n; ::_thesis: for L being non trivial ZeroStr for p being Polynomial of n,L st HC (p,O) <> 0. L holds HT (p,O) in Support (HM (p,O)) let L be non trivial ZeroStr ; ::_thesis: for p being Polynomial of n,L st HC (p,O) <> 0. L holds HT (p,O) in Support (HM (p,O)) let p be Polynomial of n,L; ::_thesis: ( HC (p,O) <> 0. L implies HT (p,O) in Support (HM (p,O)) ) assume HC (p,O) <> 0. L ; ::_thesis: HT (p,O) in Support (HM (p,O)) then (HM (p,O)) . (HT (p,O)) <> 0. L by Lm8; hence HT (p,O) in Support (HM (p,O)) by POLYNOM1:def_3; ::_thesis: verum end; Lm10: for n being Ordinal for O being connected TermOrder of n for L being non trivial ZeroStr for p being Polynomial of n,L st HC (p,O) = 0. L holds Support (HM (p,O)) = {} proof let n be Ordinal; ::_thesis: for O being connected TermOrder of n for L being non trivial ZeroStr for p being Polynomial of n,L st HC (p,O) = 0. L holds Support (HM (p,O)) = {} let O be connected TermOrder of n; ::_thesis: for L being non trivial ZeroStr for p being Polynomial of n,L st HC (p,O) = 0. L holds Support (HM (p,O)) = {} let L be non trivial ZeroStr ; ::_thesis: for p being Polynomial of n,L st HC (p,O) = 0. L holds Support (HM (p,O)) = {} let p be Polynomial of n,L; ::_thesis: ( HC (p,O) = 0. L implies Support (HM (p,O)) = {} ) assume A1: HC (p,O) = 0. L ; ::_thesis: Support (HM (p,O)) = {} then p = 0_ (n,L) by Lm7; then Support p = {} by POLYNOM7:1; then A2: HT (p,O) = EmptyBag n by Def6; A3: term (HM (p,O)) = EmptyBag n by A1, POLYNOM7:8; now__::_thesis:_not_Support_(HM_(p,O))_<>_{} assume Support (HM (p,O)) <> {} ; ::_thesis: contradiction then Support (HM (p,O)) = {(term (HM (p,O)))} by POLYNOM7:7; then term (HM (p,O)) in Support (HM (p,O)) by TARSKI:def_1; then (HM (p,O)) . (EmptyBag n) <> 0. L by A3, POLYNOM1:def_3; hence contradiction by A1, A2, Lm8; ::_thesis: verum end; hence Support (HM (p,O)) = {} ; ::_thesis: verum end; registration let n be Ordinal; let T be connected TermOrder of n; let L be non trivial ZeroStr ; let p be non-zero Polynomial of n,L; cluster HM (p,T) -> non-zero ; coherence HM (p,T) is non-zero proof set O = T; now__::_thesis:_(_(_HC_(p,T)_<>_0._L_&_HM_(p,T)_is_non-zero_)_or_(_HC_(p,T)_=_0._L_&_HM_(p,T)_is_non-zero_)_) percases ( HC (p,T) <> 0. L or HC (p,T) = 0. L ) ; case HC (p,T) <> 0. L ; ::_thesis: HM (p,T) is non-zero then HT (p,T) in Support (HM (p,T)) by Lm9; then HM (p,T) <> 0_ (n,L) by POLYNOM7:1; hence HM (p,T) is non-zero by POLYNOM7:def_1; ::_thesis: verum end; case HC (p,T) = 0. L ; ::_thesis: HM (p,T) is non-zero then p = 0_ (n,L) by Lm7; hence HM (p,T) is non-zero by POLYNOM7:def_1; ::_thesis: verum end; end; end; hence HM (p,T) is non-zero ; ::_thesis: verum end; cluster HC (p,T) -> non zero ; coherence not HC (p,T) is zero proof set O = T; set a = HC (p,T); now__::_thesis:_not_HC_(p,T)_=_0._L assume HC (p,T) = 0. L ; ::_thesis: contradiction then not HT (p,T) in Support p by POLYNOM1:def_3; then Support p = {} by Def6; then p = 0_ (n,L) by POLYNOM7:1; hence contradiction by POLYNOM7:def_1; ::_thesis: verum end; hence not HC (p,T) is zero by STRUCT_0:def_12; ::_thesis: verum end; end; Lm11: for n being Ordinal for O being connected TermOrder of n for L being non empty ZeroStr for m being Monomial of n,L holds ( HT (m,O) = term m & HC (m,O) = coefficient m & HM (m,O) = m ) proof let n be Ordinal; ::_thesis: for O being connected TermOrder of n for L being non empty ZeroStr for m being Monomial of n,L holds ( HT (m,O) = term m & HC (m,O) = coefficient m & HM (m,O) = m ) let O be connected TermOrder of n; ::_thesis: for L being non empty ZeroStr for m being Monomial of n,L holds ( HT (m,O) = term m & HC (m,O) = coefficient m & HM (m,O) = m ) let L be non empty ZeroStr ; ::_thesis: for m being Monomial of n,L holds ( HT (m,O) = term m & HC (m,O) = coefficient m & HM (m,O) = m ) let m be Monomial of n,L; ::_thesis: ( HT (m,O) = term m & HC (m,O) = coefficient m & HM (m,O) = m ) percases ( Support m = {} or ex b being bag of n st Support m = {b} ) by POLYNOM7:6; supposeA1: Support m = {} ; ::_thesis: ( HT (m,O) = term m & HC (m,O) = coefficient m & HM (m,O) = m ) hence A2: term m = EmptyBag n by POLYNOM7:def_5 .= HT (m,O) by A1, Def6 ; ::_thesis: ( HC (m,O) = coefficient m & HM (m,O) = m ) hence HC (m,O) = coefficient m by POLYNOM7:def_6; ::_thesis: HM (m,O) = m hence HM (m,O) = m by A2, POLYNOM7:11; ::_thesis: verum end; supposeA3: ex b being bag of n st Support m = {b} ; ::_thesis: ( HT (m,O) = term m & HC (m,O) = coefficient m & HM (m,O) = m ) then consider b being bag of n such that A4: Support m = {b} ; b in Support m by A4, TARSKI:def_1; then A5: m . b <> 0. L by POLYNOM1:def_3; HT (m,O) in Support m by A3, Def6; hence A6: HT (m,O) = b by A4, TARSKI:def_1 .= term m by A5, POLYNOM7:def_5 ; ::_thesis: ( HC (m,O) = coefficient m & HM (m,O) = m ) hence HC (m,O) = coefficient m by POLYNOM7:def_6; ::_thesis: HM (m,O) = m hence HM (m,O) = m by A6, POLYNOM7:11; ::_thesis: verum end; end; end; theorem :: TERMORD:17 for n being Ordinal for T being connected TermOrder of n for L being non empty ZeroStr for p being Polynomial of n,L holds ( HC (p,T) = 0. L iff p = 0_ (n,L) ) by Lm7; theorem :: TERMORD:18 for n being Ordinal for T being connected TermOrder of n for L being non trivial ZeroStr for p being Polynomial of n,L holds (HM (p,T)) . (HT (p,T)) = p . (HT (p,T)) by Lm8; theorem Th19: :: TERMORD:19 for n being Ordinal for T being connected TermOrder of n for L being non trivial ZeroStr for p being Polynomial of n,L for b being bag of n st b <> HT (p,T) holds (HM (p,T)) . b = 0. L proof let n be Ordinal; ::_thesis: for T being connected TermOrder of n for L being non trivial ZeroStr for p being Polynomial of n,L for b being bag of n st b <> HT (p,T) holds (HM (p,T)) . b = 0. L let O be connected TermOrder of n; ::_thesis: for L being non trivial ZeroStr for p being Polynomial of n,L for b being bag of n st b <> HT (p,O) holds (HM (p,O)) . b = 0. L let L be non trivial ZeroStr ; ::_thesis: for p being Polynomial of n,L for b being bag of n st b <> HT (p,O) holds (HM (p,O)) . b = 0. L let p be Polynomial of n,L; ::_thesis: for b being bag of n st b <> HT (p,O) holds (HM (p,O)) . b = 0. L let b be bag of n; ::_thesis: ( b <> HT (p,O) implies (HM (p,O)) . b = 0. L ) assume A1: b <> HT (p,O) ; ::_thesis: (HM (p,O)) . b = 0. L percases ( Support (HM (p,O)) = {} or ex b being bag of n st Support (HM (p,O)) = {b} ) by POLYNOM7:6; suppose Support (HM (p,O)) = {} ; ::_thesis: (HM (p,O)) . b = 0. L then HM (p,O) = 0_ (n,L) by POLYNOM7:1; hence (HM (p,O)) . b = 0. L by POLYNOM1:22; ::_thesis: verum end; suppose ex b being bag of n st Support (HM (p,O)) = {b} ; ::_thesis: (HM (p,O)) . b = 0. L then consider b1 being bag of n such that A2: Support (HM (p,O)) = {b1} ; A3: b is Element of Bags n by PRE_POLY:def_12; now__::_thesis:_(_(_HC_(p,O)_<>_0._L_&_(HM_(p,O))_._b_=_0._L_)_or_(_HC_(p,O)_=_0._L_&_(HM_(p,O))_._b_=_0._L_)_) percases ( HC (p,O) <> 0. L or HC (p,O) = 0. L ) ; case HC (p,O) <> 0. L ; ::_thesis: (HM (p,O)) . b = 0. L then HT (p,O) in {b1} by A2, Lm9; then b1 <> b by A1, TARSKI:def_1; then not b in {b1} by TARSKI:def_1; hence (HM (p,O)) . b = 0. L by A2, A3, POLYNOM1:def_3; ::_thesis: verum end; case HC (p,O) = 0. L ; ::_thesis: (HM (p,O)) . b = 0. L then Support (HM (p,O)) = {} by Lm10; then HM (p,O) = 0_ (n,L) by POLYNOM7:1; hence (HM (p,O)) . b = 0. L by POLYNOM1:22; ::_thesis: verum end; end; end; hence (HM (p,O)) . b = 0. L ; ::_thesis: verum end; end; end; Lm12: for n being Ordinal for O being connected TermOrder of n for L being non trivial ZeroStr for p being Polynomial of n,L holds ( Support (HM (p,O)) = {} or Support (HM (p,O)) = {(HT (p,O))} ) proof let n be Ordinal; ::_thesis: for O being connected TermOrder of n for L being non trivial ZeroStr for p being Polynomial of n,L holds ( Support (HM (p,O)) = {} or Support (HM (p,O)) = {(HT (p,O))} ) let O be connected TermOrder of n; ::_thesis: for L being non trivial ZeroStr for p being Polynomial of n,L holds ( Support (HM (p,O)) = {} or Support (HM (p,O)) = {(HT (p,O))} ) let L be non trivial ZeroStr ; ::_thesis: for p being Polynomial of n,L holds ( Support (HM (p,O)) = {} or Support (HM (p,O)) = {(HT (p,O))} ) let p be Polynomial of n,L; ::_thesis: ( Support (HM (p,O)) = {} or Support (HM (p,O)) = {(HT (p,O))} ) assume A1: not Support (HM (p,O)) = {} ; ::_thesis: Support (HM (p,O)) = {(HT (p,O))} then A2: ex b being bag of n st Support (HM (p,O)) = {b} by POLYNOM7:6; now__::_thesis:_(_(_HC_(p,O)_=_0._L_&_Support_(HM_(p,O))_=_{(HT_(p,O))}_)_or_(_HC_(p,O)_<>_0._L_&_Support_(HM_(p,O))_=_{(HT_(p,O))}_)_) percases ( HC (p,O) = 0. L or HC (p,O) <> 0. L ) ; case HC (p,O) = 0. L ; ::_thesis: Support (HM (p,O)) = {(HT (p,O))} hence Support (HM (p,O)) = {(HT (p,O))} by A1, Lm10; ::_thesis: verum end; case HC (p,O) <> 0. L ; ::_thesis: Support (HM (p,O)) = {(HT (p,O))} then HT (p,O) in Support (HM (p,O)) by Lm9; hence Support (HM (p,O)) = {(HT (p,O))} by A2, TARSKI:def_1; ::_thesis: verum end; end; end; hence Support (HM (p,O)) = {(HT (p,O))} ; ::_thesis: verum end; theorem :: TERMORD:20 for n being Ordinal for T being connected TermOrder of n for L being non trivial ZeroStr for p being Polynomial of n,L holds Support (HM (p,T)) c= Support p proof let n be Ordinal; ::_thesis: for T being connected TermOrder of n for L being non trivial ZeroStr for p being Polynomial of n,L holds Support (HM (p,T)) c= Support p let O be connected TermOrder of n; ::_thesis: for L being non trivial ZeroStr for p being Polynomial of n,L holds Support (HM (p,O)) c= Support p let L be non trivial ZeroStr ; ::_thesis: for p being Polynomial of n,L holds Support (HM (p,O)) c= Support p let p be Polynomial of n,L; ::_thesis: Support (HM (p,O)) c= Support p now__::_thesis:_for_u_being_set_st_u_in_Support_(HM_(p,O))_holds_ u_in_Support_p let u be set ; ::_thesis: ( u in Support (HM (p,O)) implies u in Support p ) assume A1: u in Support (HM (p,O)) ; ::_thesis: u in Support p now__::_thesis:_(_(_u_in_{}_&_u_in_Support_p_)_or_(_u_in_{(HT_(p,O))}_&_u_in_Support_p_)_) percases ( u in {} or u in {(HT (p,O))} ) by A1, Lm12; case u in {} ; ::_thesis: u in Support p hence u in Support p ; ::_thesis: verum end; case u in {(HT (p,O))} ; ::_thesis: u in Support p then A2: u = HT (p,O) by TARSKI:def_1; now__::_thesis:_(_(_HC_(p,O)_=_0._L_&_contradiction_)_or_(_HC_(p,O)_<>_0._L_&_u_in_Support_p_)_) percases ( HC (p,O) = 0. L or HC (p,O) <> 0. L ) ; case HC (p,O) = 0. L ; ::_thesis: contradiction then (HM (p,O)) . (HT (p,O)) = 0. L by Lm8; hence contradiction by A1, A2, POLYNOM1:def_3; ::_thesis: verum end; case HC (p,O) <> 0. L ; ::_thesis: u in Support p hence u in Support p by A2, POLYNOM1:def_3; ::_thesis: verum end; end; end; hence u in Support p ; ::_thesis: verum end; end; end; hence u in Support p ; ::_thesis: verum end; hence Support (HM (p,O)) c= Support p by TARSKI:def_3; ::_thesis: verum end; theorem :: TERMORD:21 for n being Ordinal for T being connected TermOrder of n for L being non trivial ZeroStr for p being Polynomial of n,L holds ( Support (HM (p,T)) = {} or Support (HM (p,T)) = {(HT (p,T))} ) by Lm12; theorem :: TERMORD:22 for n being Ordinal for T being connected TermOrder of n for L being non trivial ZeroStr for p being Polynomial of n,L holds ( term (HM (p,T)) = HT (p,T) & coefficient (HM (p,T)) = HC (p,T) ) proof let n be Ordinal; ::_thesis: for T being connected TermOrder of n for L being non trivial ZeroStr for p being Polynomial of n,L holds ( term (HM (p,T)) = HT (p,T) & coefficient (HM (p,T)) = HC (p,T) ) let O be connected TermOrder of n; ::_thesis: for L being non trivial ZeroStr for p being Polynomial of n,L holds ( term (HM (p,O)) = HT (p,O) & coefficient (HM (p,O)) = HC (p,O) ) let L be non trivial ZeroStr ; ::_thesis: for p being Polynomial of n,L holds ( term (HM (p,O)) = HT (p,O) & coefficient (HM (p,O)) = HC (p,O) ) let p be Polynomial of n,L; ::_thesis: ( term (HM (p,O)) = HT (p,O) & coefficient (HM (p,O)) = HC (p,O) ) percases ( not HC (p,O) is zero or HC (p,O) is zero ) ; suppose not HC (p,O) is zero ; ::_thesis: ( term (HM (p,O)) = HT (p,O) & coefficient (HM (p,O)) = HC (p,O) ) then reconsider a = HC (p,O) as non zero Element of L ; term (Monom (a,(HT (p,O)))) = HT (p,O) by POLYNOM7:10; hence ( term (HM (p,O)) = HT (p,O) & coefficient (HM (p,O)) = HC (p,O) ) by POLYNOM7:9; ::_thesis: verum end; supposeA1: HC (p,O) is zero ; ::_thesis: ( term (HM (p,O)) = HT (p,O) & coefficient (HM (p,O)) = HC (p,O) ) now__::_thesis:_(_(_not_p_is_non-zero_&_term_(HM_(p,O))_=_HT_(p,O)_&_coefficient_(HM_(p,O))_=_HC_(p,O)_)_or_(_p_is_non-zero_&_term_(HM_(p,O))_=_HT_(p,O)_&_coefficient_(HM_(p,O))_=_HC_(p,O)_)_) percases ( not p is non-zero or p is non-zero ) ; case not p is non-zero ; ::_thesis: ( term (HM (p,O)) = HT (p,O) & coefficient (HM (p,O)) = HC (p,O) ) then p = 0_ (n,L) by POLYNOM7:def_1; then Support p = {} by POLYNOM7:1; then HT (p,O) = EmptyBag n by Def6 .= term (Monom ((0. L),(HT (p,O)))) by POLYNOM7:8 .= term (HM (p,O)) by A1, STRUCT_0:def_12 ; hence ( term (HM (p,O)) = HT (p,O) & coefficient (HM (p,O)) = HC (p,O) ) by POLYNOM7:9; ::_thesis: verum end; case p is non-zero ; ::_thesis: ( term (HM (p,O)) = HT (p,O) & coefficient (HM (p,O)) = HC (p,O) ) then reconsider p = p as non-zero Polynomial of n,L ; not HC (p,O) is zero ; hence ( term (HM (p,O)) = HT (p,O) & coefficient (HM (p,O)) = HC (p,O) ) by A1; ::_thesis: verum end; end; end; hence ( term (HM (p,O)) = HT (p,O) & coefficient (HM (p,O)) = HC (p,O) ) ; ::_thesis: verum end; end; end; theorem :: TERMORD:23 for n being Ordinal for T being connected TermOrder of n for L being non empty ZeroStr for m being Monomial of n,L holds ( HT (m,T) = term m & HC (m,T) = coefficient m & HM (m,T) = m ) by Lm11; theorem :: TERMORD:24 for n being Ordinal for T being connected TermOrder of n for L being non empty ZeroStr for c being ConstPoly of n,L holds ( HT (c,T) = EmptyBag n & HC (c,T) = c . (EmptyBag n) ) proof let n be Ordinal; ::_thesis: for T being connected TermOrder of n for L being non empty ZeroStr for c being ConstPoly of n,L holds ( HT (c,T) = EmptyBag n & HC (c,T) = c . (EmptyBag n) ) let O be connected TermOrder of n; ::_thesis: for L being non empty ZeroStr for c being ConstPoly of n,L holds ( HT (c,O) = EmptyBag n & HC (c,O) = c . (EmptyBag n) ) let L be non empty ZeroStr ; ::_thesis: for c being ConstPoly of n,L holds ( HT (c,O) = EmptyBag n & HC (c,O) = c . (EmptyBag n) ) let c be ConstPoly of n,L; ::_thesis: ( HT (c,O) = EmptyBag n & HC (c,O) = c . (EmptyBag n) ) thus HT (c,O) = term c by Lm11 .= EmptyBag n by POLYNOM7:16 ; ::_thesis: HC (c,O) = c . (EmptyBag n) thus HC (c,O) = coefficient c by Lm11 .= c . (EmptyBag n) by POLYNOM7:16 ; ::_thesis: verum end; theorem :: TERMORD:25 for n being Ordinal for T being connected TermOrder of n for L being non empty ZeroStr for a being Element of L holds ( HT ((a | (n,L)),T) = EmptyBag n & HC ((a | (n,L)),T) = a ) proof let n be Ordinal; ::_thesis: for T being connected TermOrder of n for L being non empty ZeroStr for a being Element of L holds ( HT ((a | (n,L)),T) = EmptyBag n & HC ((a | (n,L)),T) = a ) let O be connected TermOrder of n; ::_thesis: for L being non empty ZeroStr for a being Element of L holds ( HT ((a | (n,L)),O) = EmptyBag n & HC ((a | (n,L)),O) = a ) let L be non empty ZeroStr ; ::_thesis: for a being Element of L holds ( HT ((a | (n,L)),O) = EmptyBag n & HC ((a | (n,L)),O) = a ) let a be Element of L; ::_thesis: ( HT ((a | (n,L)),O) = EmptyBag n & HC ((a | (n,L)),O) = a ) set p = a | (n,L); thus HT ((a | (n,L)),O) = term (a | (n,L)) by Lm11 .= EmptyBag n by POLYNOM7:23 ; ::_thesis: HC ((a | (n,L)),O) = a thus HC ((a | (n,L)),O) = coefficient (a | (n,L)) by Lm11 .= a by POLYNOM7:23 ; ::_thesis: verum end; theorem Th26: :: TERMORD:26 for n being Ordinal for T being connected TermOrder of n for L being non trivial ZeroStr for p being Polynomial of n,L holds HT ((HM (p,T)),T) = HT (p,T) proof let n be Ordinal; ::_thesis: for T being connected TermOrder of n for L being non trivial ZeroStr for p being Polynomial of n,L holds HT ((HM (p,T)),T) = HT (p,T) let O be connected TermOrder of n; ::_thesis: for L being non trivial ZeroStr for p being Polynomial of n,L holds HT ((HM (p,O)),O) = HT (p,O) let L be non trivial ZeroStr ; ::_thesis: for p being Polynomial of n,L holds HT ((HM (p,O)),O) = HT (p,O) let p be Polynomial of n,L; ::_thesis: HT ((HM (p,O)),O) = HT (p,O) percases ( not HC (p,O) is zero or HC (p,O) is zero ) ; suppose not HC (p,O) is zero ; ::_thesis: HT ((HM (p,O)),O) = HT (p,O) then reconsider a = HC (p,O) as non zero Element of L ; thus HT ((HM (p,O)),O) = term (Monom (a,(HT (p,O)))) by Lm11 .= HT (p,O) by POLYNOM7:10 ; ::_thesis: verum end; supposeA1: HC (p,O) is zero ; ::_thesis: HT ((HM (p,O)),O) = HT (p,O) now__::_thesis:_(_(_not_p_is_non-zero_&_HT_((HM_(p,O)),O)_=_HT_(p,O)_)_or_(_p_is_non-zero_&_HT_((HM_(p,O)),O)_=_HT_(p,O)_)_) percases ( not p is non-zero or p is non-zero ) ; case not p is non-zero ; ::_thesis: HT ((HM (p,O)),O) = HT (p,O) then p = 0_ (n,L) by POLYNOM7:def_1; then Support p = {} by POLYNOM7:1; then HT (p,O) = EmptyBag n by Def6 .= term (Monom ((0. L),(HT (p,O)))) by POLYNOM7:8 .= term (HM (p,O)) by A1, STRUCT_0:def_12 ; hence HT ((HM (p,O)),O) = HT (p,O) by Lm11; ::_thesis: verum end; case p is non-zero ; ::_thesis: HT ((HM (p,O)),O) = HT (p,O) then reconsider p = p as non-zero Polynomial of n,L ; not HC (p,O) is zero ; hence HT ((HM (p,O)),O) = HT (p,O) by A1; ::_thesis: verum end; end; end; hence HT ((HM (p,O)),O) = HT (p,O) ; ::_thesis: verum end; end; end; theorem :: TERMORD:27 for n being Ordinal for T being connected TermOrder of n for L being non trivial ZeroStr for p being Polynomial of n,L holds HC ((HM (p,T)),T) = HC (p,T) proof let n be Ordinal; ::_thesis: for T being connected TermOrder of n for L being non trivial ZeroStr for p being Polynomial of n,L holds HC ((HM (p,T)),T) = HC (p,T) let O be connected TermOrder of n; ::_thesis: for L being non trivial ZeroStr for p being Polynomial of n,L holds HC ((HM (p,O)),O) = HC (p,O) let L be non trivial ZeroStr ; ::_thesis: for p being Polynomial of n,L holds HC ((HM (p,O)),O) = HC (p,O) let p be Polynomial of n,L; ::_thesis: HC ((HM (p,O)),O) = HC (p,O) thus HC ((HM (p,O)),O) = (HM (p,O)) . (HT (p,O)) by Th26 .= HC (p,O) by Lm8 ; ::_thesis: verum end; theorem :: TERMORD:28 for n being Ordinal for T being connected TermOrder of n for L being non empty ZeroStr for p being Polynomial of n,L holds HM ((HM (p,T)),T) = HM (p,T) by Lm11; Lm13: for X being set for S being Subset of X for R being Order of X st R is being_linear-order holds R linearly_orders S proof let X be set ; ::_thesis: for S being Subset of X for R being Order of X st R is being_linear-order holds R linearly_orders S let S be Subset of X; ::_thesis: for R being Order of X st R is being_linear-order holds R linearly_orders S let R be Order of X; ::_thesis: ( R is being_linear-order implies R linearly_orders S ) S c= X ; then A1: S c= field R by ORDERS_1:15; assume R is being_linear-order ; ::_thesis: R linearly_orders S hence R linearly_orders S by A1, ORDERS_1:37, ORDERS_1:38; ::_thesis: verum end; Lm14: for n being Ordinal for O being connected admissible TermOrder of n for L being non trivial right_complementable well-unital distributive add-associative right_zeroed left_zeroed doubleLoopStr for p, q being non-zero Polynomial of n,L holds (p *' q) . ((HT (p,O)) + (HT (q,O))) = (p . (HT (p,O))) * (q . (HT (q,O))) proof let n be Ordinal; ::_thesis: for O being connected admissible TermOrder of n for L being non trivial right_complementable well-unital distributive add-associative right_zeroed left_zeroed doubleLoopStr for p, q being non-zero Polynomial of n,L holds (p *' q) . ((HT (p,O)) + (HT (q,O))) = (p . (HT (p,O))) * (q . (HT (q,O))) let O be connected admissible TermOrder of n; ::_thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed left_zeroed doubleLoopStr for p, q being non-zero Polynomial of n,L holds (p *' q) . ((HT (p,O)) + (HT (q,O))) = (p . (HT (p,O))) * (q . (HT (q,O))) let L be non trivial right_complementable well-unital distributive add-associative right_zeroed left_zeroed doubleLoopStr ; ::_thesis: for p, q being non-zero Polynomial of n,L holds (p *' q) . ((HT (p,O)) + (HT (q,O))) = (p . (HT (p,O))) * (q . (HT (q,O))) let p, q be non-zero Polynomial of n,L; ::_thesis: (p *' q) . ((HT (p,O)) + (HT (q,O))) = (p . (HT (p,O))) * (q . (HT (q,O))) set b = (HT (p,O)) + (HT (q,O)); consider s being FinSequence of L such that A1: (p *' q) . ((HT (p,O)) + (HT (q,O))) = Sum s and A2: len s = len (decomp ((HT (p,O)) + (HT (q,O)))) and A3: for k being Element of NAT st k in dom s holds ex b1, b2 being bag of n st ( (decomp ((HT (p,O)) + (HT (q,O)))) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) by POLYNOM1:def_9; consider S being non empty finite Subset of (Bags n) such that A4: divisors ((HT (p,O)) + (HT (q,O))) = SgmX ((BagOrder n),S) and A5: for p being bag of n holds ( p in S iff p divides (HT (p,O)) + (HT (q,O)) ) by PRE_POLY:def_16; set sgm = SgmX ((BagOrder n),S); A6: BagOrder n linearly_orders S by Lm13; HT (p,O) divides (HT (p,O)) + (HT (q,O)) by PRE_POLY:50; then HT (p,O) in S by A5; then HT (p,O) in rng (SgmX ((BagOrder n),S)) by A6, PRE_POLY:def_2; then consider i being set such that A7: i in dom (SgmX ((BagOrder n),S)) and A8: (SgmX ((BagOrder n),S)) . i = HT (p,O) by FUNCT_1:def_3; A9: i in dom (decomp ((HT (p,O)) + (HT (q,O)))) by A4, A7, PRE_POLY:def_17; (divisors ((HT (p,O)) + (HT (q,O)))) /. i = HT (p,O) by A4, A7, A8, PARTFUN1:def_6; then A10: (decomp ((HT (p,O)) + (HT (q,O)))) /. i = <*(HT (p,O)),(((HT (p,O)) + (HT (q,O))) -' (HT (p,O)))*> by A9, PRE_POLY:def_17; then A11: (decomp ((HT (p,O)) + (HT (q,O)))) /. i = <*(HT (p,O)),(HT (q,O))*> by PRE_POLY:48; A12: dom s = Seg (len (decomp ((HT (p,O)) + (HT (q,O))))) by A2, FINSEQ_1:def_3 .= dom (decomp ((HT (p,O)) + (HT (q,O)))) by FINSEQ_1:def_3 ; then A13: i in dom s by A4, A7, PRE_POLY:def_17; reconsider i = i as Element of NAT by A7; consider b1, b2 being bag of n such that A14: (decomp ((HT (p,O)) + (HT (q,O)))) /. i = <*b1,b2*> and A15: s /. i = (p . b1) * (q . b2) by A3, A13; A16: b2 = <*(HT (p,O)),(HT (q,O))*> . 2 by A11, A14, FINSEQ_1:44 .= HT (q,O) by FINSEQ_1:44 ; A17: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_s_&_k_<>_i_holds_ s_/._k_=_0._L let k be Element of NAT ; ::_thesis: ( k in dom s & k <> i implies s /. k = 0. L ) assume that A18: k in dom s and A19: k <> i ; ::_thesis: s /. k = 0. L consider b1, b2 being bag of n such that A20: (decomp ((HT (p,O)) + (HT (q,O)))) /. k = <*b1,b2*> and A21: s /. k = (p . b1) * (q . b2) by A3, A18; consider b19, b29 being bag of n such that A22: (decomp ((HT (p,O)) + (HT (q,O)))) /. k = <*b19,b29*> and A23: (HT (p,O)) + (HT (q,O)) = b19 + b29 by A12, A18, PRE_POLY:68; A24: b2 = <*b19,b29*> . 2 by A22, A20, FINSEQ_1:44 .= b29 by FINSEQ_1:44 ; A25: b1 = <*b19,b29*> . 1 by A22, A20, FINSEQ_1:44 .= b19 by FINSEQ_1:44 ; A26: now__::_thesis:_(_p_._b1_<>_0._L_implies_not_q_._b2_<>_0._L_) assume that A27: p . b1 <> 0. L and A28: q . b2 <> 0. L ; ::_thesis: contradiction b1 is Element of Bags n by PRE_POLY:def_12; then b1 in Support p by A27, POLYNOM1:def_3; then b1 <= HT (p,O),O by Def6; then A29: [b1,(HT (p,O))] in O by Def2; b2 is Element of Bags n by PRE_POLY:def_12; then b2 in Support q by A28, POLYNOM1:def_3; then b2 <= HT (q,O),O by Def6; then A30: [b2,(HT (q,O))] in O by Def2; A31: now__::_thesis:_(_b1_=_HT_(p,O)_implies_not_b2_=_HT_(q,O)_) assume ( b1 = HT (p,O) & b2 = HT (q,O) ) ; ::_thesis: contradiction then (decomp ((HT (p,O)) + (HT (q,O)))) . k = <*(HT (p,O)),(HT (q,O))*> by A12, A18, A20, PARTFUN1:def_6 .= (decomp ((HT (p,O)) + (HT (q,O)))) /. i by A10, PRE_POLY:48 .= (decomp ((HT (p,O)) + (HT (q,O)))) . i by A9, PARTFUN1:def_6 ; hence contradiction by A9, A12, A18, A19, FUNCT_1:def_4; ::_thesis: verum end; now__::_thesis:_(_(_b1_<>_HT_(p,O)_&_contradiction_)_or_(_b2_<>_HT_(q,O)_&_contradiction_)_) percases ( b1 <> HT (p,O) or b2 <> HT (q,O) ) by A31; caseA32: b1 <> HT (p,O) ; ::_thesis: contradiction A33: now__::_thesis:_not_b1_+_b2_=_(HT_(p,O))_+_b2 assume b1 + b2 = (HT (p,O)) + b2 ; ::_thesis: contradiction then b1 = ((HT (p,O)) + b2) -' b2 by PRE_POLY:48; hence contradiction by A32, PRE_POLY:48; ::_thesis: verum end; A34: ( (HT (p,O)) + b2 is Element of Bags n & (HT (p,O)) + (HT (q,O)) is Element of Bags n ) by PRE_POLY:def_12; ( [((HT (p,O)) + (HT (q,O))),((HT (p,O)) + b2)] in O & [((HT (p,O)) + b2),((HT (p,O)) + (HT (q,O)))] in O ) by A23, A25, A24, A29, A30, BAGORDER:def_5; hence contradiction by A23, A25, A24, A33, A34, ORDERS_1:4; ::_thesis: verum end; caseA35: b2 <> HT (q,O) ; ::_thesis: contradiction A36: now__::_thesis:_not_b2_+_b1_=_(HT_(q,O))_+_b1 assume b2 + b1 = (HT (q,O)) + b1 ; ::_thesis: contradiction then b2 = ((HT (q,O)) + b1) -' b1 by PRE_POLY:48; hence contradiction by A35, PRE_POLY:48; ::_thesis: verum end; A37: ( (HT (q,O)) + b1 is Element of Bags n & (HT (p,O)) + (HT (q,O)) is Element of Bags n ) by PRE_POLY:def_12; ( [((HT (p,O)) + (HT (q,O))),((HT (q,O)) + b1)] in O & [((HT (q,O)) + b1),((HT (p,O)) + (HT (q,O)))] in O ) by A23, A25, A24, A29, A30, BAGORDER:def_5; hence contradiction by A23, A25, A24, A36, A37, ORDERS_1:4; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; now__::_thesis:_(_(_p_._b1_=_0._L_&_(p_._b1)_*_(q_._b2)_=_0._L_)_or_(_q_._b2_=_0._L_&_(p_._b1)_*_(q_._b2)_=_0._L_)_) percases ( p . b1 = 0. L or q . b2 = 0. L ) by A26; case p . b1 = 0. L ; ::_thesis: (p . b1) * (q . b2) = 0. L hence (p . b1) * (q . b2) = 0. L by BINOM:1; ::_thesis: verum end; case q . b2 = 0. L ; ::_thesis: (p . b1) * (q . b2) = 0. L hence (p . b1) * (q . b2) = 0. L by BINOM:2; ::_thesis: verum end; end; end; hence s /. k = 0. L by A21; ::_thesis: verum end; b1 = <*(HT (p,O)),(HT (q,O))*> . 1 by A11, A14, FINSEQ_1:44 .= HT (p,O) by FINSEQ_1:44 ; hence (p *' q) . ((HT (p,O)) + (HT (q,O))) = (p . (HT (p,O))) * (q . (HT (q,O))) by A1, A13, A17, A15, A16, POLYNOM2:3; ::_thesis: verum end; theorem Th29: :: TERMORD:29 for n being Ordinal for T being connected admissible TermOrder of n for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like left_zeroed doubleLoopStr for p, q being non-zero Polynomial of n,L holds (HT (p,T)) + (HT (q,T)) in Support (p *' q) proof let n be Ordinal; ::_thesis: for T being connected admissible TermOrder of n for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like left_zeroed doubleLoopStr for p, q being non-zero Polynomial of n,L holds (HT (p,T)) + (HT (q,T)) in Support (p *' q) let O be connected admissible TermOrder of n; ::_thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like left_zeroed doubleLoopStr for p, q being non-zero Polynomial of n,L holds (HT (p,O)) + (HT (q,O)) in Support (p *' q) let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like left_zeroed doubleLoopStr ; ::_thesis: for p, q being non-zero Polynomial of n,L holds (HT (p,O)) + (HT (q,O)) in Support (p *' q) let p, q be non-zero Polynomial of n,L; ::_thesis: (HT (p,O)) + (HT (q,O)) in Support (p *' q) set b = (HT (p,O)) + (HT (q,O)); assume A1: not (HT (p,O)) + (HT (q,O)) in Support (p *' q) ; ::_thesis: contradiction p <> 0_ (n,L) by POLYNOM7:def_1; then Support p <> {} by POLYNOM7:1; then HT (p,O) in Support p by Def6; then A2: p . (HT (p,O)) <> 0. L by POLYNOM1:def_3; q <> 0_ (n,L) by POLYNOM7:def_1; then Support q <> {} by POLYNOM7:1; then HT (q,O) in Support q by Def6; then A3: q . (HT (q,O)) <> 0. L by POLYNOM1:def_3; (HT (p,O)) + (HT (q,O)) is Element of Bags n by PRE_POLY:def_12; then (p *' q) . ((HT (p,O)) + (HT (q,O))) = 0. L by A1, POLYNOM1:def_3; then (p . (HT (p,O))) * (q . (HT (q,O))) = 0. L by Lm14; hence contradiction by A2, A3, VECTSP_2:def_1; ::_thesis: verum end; theorem Th30: :: TERMORD:30 for n being Ordinal for L being non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr for p, q being Polynomial of n,L holds Support (p *' q) c= { (s + t) where s, t is Element of Bags n : ( s in Support p & t in Support q ) } proof let n be Ordinal; ::_thesis: for L being non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr for p, q being Polynomial of n,L holds Support (p *' q) c= { (s + t) where s, t is Element of Bags n : ( s in Support p & t in Support q ) } let L be non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q being Polynomial of n,L holds Support (p *' q) c= { (s + t) where s, t is Element of Bags n : ( s in Support p & t in Support q ) } let p, q be Polynomial of n,L; ::_thesis: Support (p *' q) c= { (s + t) where s, t is Element of Bags n : ( s in Support p & t in Support q ) } A1: now__::_thesis:_for_b_being_bag_of_n_st_b_in_Support_(p_*'_q)_holds_ ex_s,_t_being_bag_of_n_st_ (_s_in_Support_p_&_t_in_Support_q_&_b_=_s_+_t_) let b be bag of n; ::_thesis: ( b in Support (p *' q) implies ex s, t being bag of n st ( s in Support p & t in Support q & b = s + t ) ) consider s being FinSequence of L such that A2: (p *' q) . b = Sum s and A3: len s = len (decomp b) and A4: 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) * (q . b2) ) by POLYNOM1:def_9; A5: dom s = Seg (len (decomp b)) by A3, FINSEQ_1:def_3 .= dom (decomp b) by FINSEQ_1:def_3 ; assume A6: b in Support (p *' q) ; ::_thesis: ex s, t being bag of n st ( s in Support p & t in Support q & b = s + t ) now__::_thesis:_(_(_dom_s_=_{}_&_contradiction_)_or_(_dom_s_<>_{}_&_ex_s,_t_being_bag_of_n_st_ (_s_in_Support_p_&_t_in_Support_q_&_b_=_s_+_t_)_)_) percases ( dom s = {} or dom s <> {} ) ; case dom s = {} ; ::_thesis: contradiction then Seg (len s) = {} by FINSEQ_1:def_3; then len s = 0 ; hence contradiction by A3; ::_thesis: verum end; caseA7: dom s <> {} ; ::_thesis: ex s, t being bag of n st ( s in Support p & t in Support q & b = s + t ) set k = the Element of dom s; the Element of dom s in dom s by A7; then reconsider k = the Element of dom s as Element of NAT ; now__::_thesis:_ex_k_being_Element_of_dom_(decomp_b)_ex_b1,_b2_being_bag_of_n_st_ (_(decomp_b)_/._k_=_<*b1,b2*>_&_p_._b1_<>_0._L_&_q_._b2_<>_0._L_) assume A8: for k being Element of dom (decomp b) for b1, b2 being bag of n holds ( not (decomp b) /. k = <*b1,b2*> or not p . b1 <> 0. L or not q . b2 <> 0. L ) ; ::_thesis: contradiction A9: for k being Nat st k in dom s holds s /. k = 0. L proof let k be Nat; ::_thesis: ( k in dom s implies s /. k = 0. L ) assume A10: k in dom s ; ::_thesis: s /. k = 0. L then consider b1, b2 being bag of n such that A11: (decomp b) /. k = <*b1,b2*> and A12: s /. k = (p . b1) * (q . b2) by A4; now__::_thesis:_(_(_p_._b1_=_0._L_&_s_/._k_=_0._L_)_or_(_q_._b2_=_0._L_&_s_/._k_=_0._L_)_) percases ( p . b1 = 0. L or q . b2 = 0. L ) by A5, A8, A10, A11; case p . b1 = 0. L ; ::_thesis: s /. k = 0. L hence s /. k = 0. L by A12, BINOM:1; ::_thesis: verum end; case q . b2 = 0. L ; ::_thesis: s /. k = 0. L hence s /. k = 0. L by A12, BINOM:2; ::_thesis: verum end; end; end; hence s /. k = 0. L ; ::_thesis: verum end; then for k9 being Element of NAT st k9 in dom s & k9 <> k holds s /. k9 = 0. L ; then Sum s = s /. k by A7, POLYNOM2:3 .= 0. L by A7, A9 ; hence contradiction by A6, A2, POLYNOM1:def_3; ::_thesis: verum end; then consider k being Element of dom (decomp b), b1, b2 being bag of n such that A13: (decomp b) /. k = <*b1,b2*> and A14: p . b1 <> 0. L and A15: q . b2 <> 0. L ; k in dom (decomp b) by A5, A7; then reconsider k = k as Element of NAT ; consider b19, b29 being bag of n such that A16: (decomp b) /. k = <*b19,b29*> and A17: b = b19 + b29 by A5, A7, PRE_POLY:68; A18: b29 = <*b1,b2*> . 2 by A13, A16, FINSEQ_1:44 .= b2 by FINSEQ_1:44 ; b2 is Element of Bags n by PRE_POLY:def_12; then A19: b2 in Support q by A15, POLYNOM1:def_3; b1 is Element of Bags n by PRE_POLY:def_12; then A20: b1 in Support p by A14, POLYNOM1:def_3; b19 = <*b1,b2*> . 1 by A13, A16, FINSEQ_1:44 .= b1 by FINSEQ_1:44 ; hence ex s, t being bag of n st ( s in Support p & t in Support q & b = s + t ) by A20, A19, A17, A18; ::_thesis: verum end; end; end; hence ex s, t being bag of n st ( s in Support p & t in Support q & b = s + t ) ; ::_thesis: verum end; now__::_thesis:_for_u_being_set_st_u_in_Support_(p_*'_q)_holds_ u_in__{__(s9_+_t9)_where_s9,_t9_is_Element_of_Bags_n_:_(_s9_in_Support_p_&_t9_in_Support_q_)__}_ let u be set ; ::_thesis: ( u in Support (p *' q) implies u in { (s9 + t9) where s9, t9 is Element of Bags n : ( s9 in Support p & t9 in Support q ) } ) assume A21: u in Support (p *' q) ; ::_thesis: u in { (s9 + t9) where s9, t9 is Element of Bags n : ( s9 in Support p & t9 in Support q ) } then reconsider u9 = u as Element of Bags n ; ex s, t being bag of n st ( s in Support p & t in Support q & u9 = s + t ) by A1, A21; hence u in { (s9 + t9) where s9, t9 is Element of Bags n : ( s9 in Support p & t9 in Support q ) } ; ::_thesis: verum end; hence Support (p *' q) c= { (s + t) where s, t is Element of Bags n : ( s in Support p & t in Support q ) } by TARSKI:def_3; ::_thesis: verum end; theorem Th31: :: TERMORD:31 for n being Ordinal for T being connected admissible TermOrder of n for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr for p, q being non-zero Polynomial of n,L holds HT ((p *' q),T) = (HT (p,T)) + (HT (q,T)) proof let n be Ordinal; ::_thesis: for T being connected admissible TermOrder of n for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr for p, q being non-zero Polynomial of n,L holds HT ((p *' q),T) = (HT (p,T)) + (HT (q,T)) let O be connected admissible TermOrder of n; ::_thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr for p, q being non-zero Polynomial of n,L holds HT ((p *' q),O) = (HT (p,O)) + (HT (q,O)) let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for p, q being non-zero Polynomial of n,L holds HT ((p *' q),O) = (HT (p,O)) + (HT (q,O)) let p, q be non-zero Polynomial of n,L; ::_thesis: HT ((p *' q),O) = (HT (p,O)) + (HT (q,O)) A1: (HT (p,O)) + (HT (q,O)) is Element of Bags n by PRE_POLY:def_12; (HT (p,O)) + (HT (q,O)) in Support (p *' q) by Th29; then (HT (p,O)) + (HT (q,O)) <= HT ((p *' q),O),O by Def6; then A2: [((HT (p,O)) + (HT (q,O))),(HT ((p *' q),O))] in O by Def2; Support (p *' q) <> {} by Th29; then A3: HT ((p *' q),O) in Support (p *' q) by Def6; Support (p *' q) c= { (s + t) where s, t is Element of Bags n : ( s in Support p & t in Support q ) } by Th30; then HT ((p *' q),O) in { (s + t) where s, t is Element of Bags n : ( s in Support p & t in Support q ) } by A3; then consider s, t being Element of Bags n such that A4: HT ((p *' q),O) = s + t and A5: s in Support p and A6: t in Support q ; s <= HT (p,O),O by A5, Def6; then [s,(HT (p,O))] in O by Def2; then A7: [(s + t),((HT (p,O)) + t)] in O by BAGORDER:def_5; t <= HT (q,O),O by A6, Def6; then [t,(HT (q,O))] in O by Def2; then A8: [(t + (HT (p,O))),((HT (p,O)) + (HT (q,O)))] in O by BAGORDER:def_5; ( s + t is Element of Bags n & (HT (p,O)) + t is Element of Bags n ) by PRE_POLY:def_12; then [(s + t),((HT (p,O)) + (HT (q,O)))] in O by A1, A7, A8, ORDERS_1:5; hence HT ((p *' q),O) = (HT (p,O)) + (HT (q,O)) by A2, A4, A1, ORDERS_1:4; ::_thesis: verum end; theorem Th32: :: TERMORD:32 for n being Ordinal for T being connected admissible TermOrder of n for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr for p, q being non-zero Polynomial of n,L holds HC ((p *' q),T) = (HC (p,T)) * (HC (q,T)) proof let n be Ordinal; ::_thesis: for T being connected admissible TermOrder of n for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr for p, q being non-zero Polynomial of n,L holds HC ((p *' q),T) = (HC (p,T)) * (HC (q,T)) let O be connected admissible TermOrder of n; ::_thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr for p, q being non-zero Polynomial of n,L holds HC ((p *' q),O) = (HC (p,O)) * (HC (q,O)) let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for p, q being non-zero Polynomial of n,L holds HC ((p *' q),O) = (HC (p,O)) * (HC (q,O)) let p, q be non-zero Polynomial of n,L; ::_thesis: HC ((p *' q),O) = (HC (p,O)) * (HC (q,O)) thus HC ((p *' q),O) = (p *' q) . ((HT (p,O)) + (HT (q,O))) by Th31 .= (HC (p,O)) * (HC (q,O)) by Lm14 ; ::_thesis: verum end; theorem :: TERMORD:33 for n being Ordinal for T being connected admissible TermOrder of n for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr for p, q being non-zero Polynomial of n,L holds HM ((p *' q),T) = (HM (p,T)) *' (HM (q,T)) proof let n be Ordinal; ::_thesis: for T being connected admissible TermOrder of n for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr for p, q being non-zero Polynomial of n,L holds HM ((p *' q),T) = (HM (p,T)) *' (HM (q,T)) let O be connected admissible TermOrder of n; ::_thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr for p, q being non-zero Polynomial of n,L holds HM ((p *' q),O) = (HM (p,O)) *' (HM (q,O)) let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for p, q being non-zero Polynomial of n,L holds HM ((p *' q),O) = (HM (p,O)) *' (HM (q,O)) let p, q be non-zero Polynomial of n,L; ::_thesis: HM ((p *' q),O) = (HM (p,O)) *' (HM (q,O)) thus HM ((p *' q),O) = Monom (((HC (p,O)) * (HC (q,O))),(HT ((p *' q),O))) by Th32 .= Monom (((HC (p,O)) * (HC (q,O))),((HT (p,O)) + (HT (q,O)))) by Th31 .= (HM (p,O)) *' (HM (q,O)) by Th3 ; ::_thesis: verum end; theorem :: TERMORD:34 for n being Ordinal for T being connected admissible TermOrder of n for L being non empty right_zeroed addLoopStr for p, q being Polynomial of n,L holds HT ((p + q),T) <= max ((HT (p,T)),(HT (q,T)),T),T proof let n be Ordinal; ::_thesis: for T being connected admissible TermOrder of n for L being non empty right_zeroed addLoopStr for p, q being Polynomial of n,L holds HT ((p + q),T) <= max ((HT (p,T)),(HT (q,T)),T),T let O be connected admissible TermOrder of n; ::_thesis: for L being non empty right_zeroed addLoopStr for p, q being Polynomial of n,L holds HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O let L be non empty right_zeroed addLoopStr ; ::_thesis: for p, q being Polynomial of n,L holds HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O let p, q be Polynomial of n,L; ::_thesis: HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O percases ( HT ((p + q),O) in Support (p + q) or not HT ((p + q),O) in Support (p + q) ) ; supposeA1: HT ((p + q),O) in Support (p + q) ; ::_thesis: HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O A2: Support (p + q) c= (Support p) \/ (Support q) by POLYNOM1:20; now__::_thesis:_(_(_HT_((p_+_q),O)_in_Support_p_&_HT_((p_+_q),O)_<=_max_((HT_(p,O)),(HT_(q,O)),O),O_)_or_(_HT_((p_+_q),O)_in_Support_q_&_HT_((p_+_q),O)_<=_max_((HT_(p,O)),(HT_(q,O)),O),O_)_) percases ( HT ((p + q),O) in Support p or HT ((p + q),O) in Support q ) by A1, A2, XBOOLE_0:def_3; caseA3: HT ((p + q),O) in Support p ; ::_thesis: HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O then A4: HT ((p + q),O) <= HT (p,O),O by Def6; now__::_thesis:_(_(_max_((HT_(p,O)),(HT_(q,O)),O)_=_HT_(p,O)_&_HT_((p_+_q),O)_<=_max_((HT_(p,O)),(HT_(q,O)),O),O_)_or_(_max_((HT_(p,O)),(HT_(q,O)),O)_=_HT_(q,O)_&_HT_((p_+_q),O)_<=_max_((HT_(p,O)),(HT_(q,O)),O),O_)_) percases ( max ((HT (p,O)),(HT (q,O)),O) = HT (p,O) or max ((HT (p,O)),(HT (q,O)),O) = HT (q,O) ) by Th12; case max ((HT (p,O)),(HT (q,O)),O) = HT (p,O) ; ::_thesis: HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O hence HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O by A3, Def6; ::_thesis: verum end; caseA5: max ((HT (p,O)),(HT (q,O)),O) = HT (q,O) ; ::_thesis: HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O then HT (p,O) <= HT (q,O),O by Th14; hence HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O by A4, A5, Th8; ::_thesis: verum end; end; end; hence HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O ; ::_thesis: verum end; caseA6: HT ((p + q),O) in Support q ; ::_thesis: HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O then A7: HT ((p + q),O) <= HT (q,O),O by Def6; now__::_thesis:_(_(_max_((HT_(p,O)),(HT_(q,O)),O)_=_HT_(q,O)_&_HT_((p_+_q),O)_<=_max_((HT_(p,O)),(HT_(q,O)),O),O_)_or_(_max_((HT_(p,O)),(HT_(q,O)),O)_=_HT_(p,O)_&_HT_((p_+_q),O)_<=_max_((HT_(p,O)),(HT_(q,O)),O),O_)_) percases ( max ((HT (p,O)),(HT (q,O)),O) = HT (q,O) or max ((HT (p,O)),(HT (q,O)),O) = HT (p,O) ) by Th12; case max ((HT (p,O)),(HT (q,O)),O) = HT (q,O) ; ::_thesis: HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O hence HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O by A6, Def6; ::_thesis: verum end; caseA8: max ((HT (p,O)),(HT (q,O)),O) = HT (p,O) ; ::_thesis: HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O then HT (q,O) <= HT (p,O),O by Th14; hence HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O by A7, A8, Th8; ::_thesis: verum end; end; end; hence HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O ; ::_thesis: verum end; end; end; hence HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O ; ::_thesis: verum end; suppose not HT ((p + q),O) in Support (p + q) ; ::_thesis: HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O then HT ((p + q),O) = EmptyBag n by Def6; then [(HT ((p + q),O)),(max ((HT (p,O)),(HT (q,O)),O))] in O by BAGORDER:def_5; hence HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O by Def2; ::_thesis: verum end; end; end; begin definition let n be Ordinal; let T be connected TermOrder of n; let L be non empty right_complementable add-associative right_zeroed addLoopStr ; let p be Polynomial of n,L; func Red (p,T) -> Polynomial of n,L equals :: TERMORD:def 9 p - (HM (p,T)); coherence p - (HM (p,T)) is Polynomial of n,L ; end; :: deftheorem defines Red TERMORD:def_9_:_ for n being Ordinal for T being connected TermOrder of n for L being non empty right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L holds Red (p,T) = p - (HM (p,T)); Lm15: for n being Ordinal for O being connected TermOrder of n for L being non trivial right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L holds not HT (p,O) in Support (Red (p,O)) proof let n be Ordinal; ::_thesis: for O being connected TermOrder of n for L being non trivial right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L holds not HT (p,O) in Support (Red (p,O)) let O be connected TermOrder of n; ::_thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L holds not HT (p,O) in Support (Red (p,O)) let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being Polynomial of n,L holds not HT (p,O) in Support (Red (p,O)) let p be Polynomial of n,L; ::_thesis: not HT (p,O) in Support (Red (p,O)) assume HT (p,O) in Support (Red (p,O)) ; ::_thesis: contradiction then (Red (p,O)) . (HT (p,O)) <> 0. L by POLYNOM1:def_3; then (p + (- (HM (p,O)))) . (HT (p,O)) <> 0. L by POLYNOM1:def_6; then (p . (HT (p,O))) + ((- (HM (p,O))) . (HT (p,O))) <> 0. L by POLYNOM1:15; then A1: (p . (HT (p,O))) + (- ((HM (p,O)) . (HT (p,O)))) <> 0. L by POLYNOM1:17; (HM (p,O)) . (HT (p,O)) = p . (HT (p,O)) by Lm8; hence contradiction by A1, RLVECT_1:def_10; ::_thesis: verum end; Lm16: for n being Ordinal for O being connected TermOrder of n for L being non trivial right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L for b being bag of n st b in Support p & b <> HT (p,O) holds b in Support (Red (p,O)) proof let n be Ordinal; ::_thesis: for O being connected TermOrder of n for L being non trivial right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L for b being bag of n st b in Support p & b <> HT (p,O) holds b in Support (Red (p,O)) let O be connected TermOrder of n; ::_thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L for b being bag of n st b in Support p & b <> HT (p,O) holds b in Support (Red (p,O)) let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being Polynomial of n,L for b being bag of n st b in Support p & b <> HT (p,O) holds b in Support (Red (p,O)) let p be Polynomial of n,L; ::_thesis: for b being bag of n st b in Support p & b <> HT (p,O) holds b in Support (Red (p,O)) let b be bag of n; ::_thesis: ( b in Support p & b <> HT (p,O) implies b in Support (Red (p,O)) ) assume that A1: b in Support p and A2: b <> HT (p,O) ; ::_thesis: b in Support (Red (p,O)) (Red (p,O)) . b = (p + (- (HM (p,O)))) . b by POLYNOM1:def_6 .= (p . b) + ((- (HM (p,O))) . b) by POLYNOM1:15 .= (p . b) + (- ((HM (p,O)) . b)) by POLYNOM1:17 .= (p . b) + (- (0. L)) by A2, Th19 .= (p . b) + (0. L) by RLVECT_1:12 .= p . b by RLVECT_1:4 ; then ( b is Element of Bags n & (Red (p,O)) . b <> 0. L ) by A1, POLYNOM1:def_3; hence b in Support (Red (p,O)) by POLYNOM1:def_3; ::_thesis: verum end; Lm17: for n being Ordinal for O being connected TermOrder of n for L being non trivial right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L holds Support (Red (p,O)) = (Support p) \ {(HT (p,O))} proof let n be Ordinal; ::_thesis: for O being connected TermOrder of n for L being non trivial right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L holds Support (Red (p,O)) = (Support p) \ {(HT (p,O))} let O be connected TermOrder of n; ::_thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L holds Support (Red (p,O)) = (Support p) \ {(HT (p,O))} let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being Polynomial of n,L holds Support (Red (p,O)) = (Support p) \ {(HT (p,O))} let p be Polynomial of n,L; ::_thesis: Support (Red (p,O)) = (Support p) \ {(HT (p,O))} A1: now__::_thesis:_for_u_being_set_st_u_in_Support_(Red_(p,O))_holds_ u_in_(Support_p)_\_{(HT_(p,O))} let u be set ; ::_thesis: ( u in Support (Red (p,O)) implies u in (Support p) \ {(HT (p,O))} ) assume A2: u in Support (Red (p,O)) ; ::_thesis: u in (Support p) \ {(HT (p,O))} then reconsider u9 = u as Element of Bags n ; reconsider u9 = u9 as bag of n ; A3: (p - (HM (p,O))) . u9 <> 0. L by A2, POLYNOM1:def_3; A4: not u9 = HT (p,O) by A2, Lm15; (p + (- (HM (p,O)))) . u9 = (p . u9) + ((- (HM (p,O))) . u9) by POLYNOM1:15 .= (p . u9) + (- ((HM (p,O)) . u9)) by POLYNOM1:17 ; then (p + (- (HM (p,O)))) . u9 = (p . u9) + (- (0. L)) by A4, Th19 .= (p . u9) + (0. L) by RLVECT_1:12 .= p . u9 by RLVECT_1:4 ; then p . u9 <> 0. L by A3, POLYNOM1:def_6; then A5: u9 in Support p by POLYNOM1:def_3; not u9 in {(HT (p,O))} by A4, TARSKI:def_1; hence u in (Support p) \ {(HT (p,O))} by A5, XBOOLE_0:def_5; ::_thesis: verum end; now__::_thesis:_for_u_being_set_st_u_in_(Support_p)_\_{(HT_(p,O))}_holds_ u_in_Support_(Red_(p,O)) let u be set ; ::_thesis: ( u in (Support p) \ {(HT (p,O))} implies u in Support (Red (p,O)) ) assume A6: u in (Support p) \ {(HT (p,O))} ; ::_thesis: u in Support (Red (p,O)) then reconsider u9 = u as Element of Bags n ; reconsider u9 = u9 as bag of n ; not u in {(HT (p,O))} by A6, XBOOLE_0:def_5; then A7: u9 <> HT (p,O) by TARSKI:def_1; u in Support p by A6, XBOOLE_0:def_5; hence u in Support (Red (p,O)) by A7, Lm16; ::_thesis: verum end; hence Support (Red (p,O)) = (Support p) \ {(HT (p,O))} by A1, TARSKI:1; ::_thesis: verum end; theorem :: TERMORD:35 for n being Ordinal for T being connected TermOrder of n for L being non trivial right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L holds Support (Red (p,T)) c= Support p proof let n be Ordinal; ::_thesis: for T being connected TermOrder of n for L being non trivial right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L holds Support (Red (p,T)) c= Support p let O be connected TermOrder of n; ::_thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L holds Support (Red (p,O)) c= Support p let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being Polynomial of n,L holds Support (Red (p,O)) c= Support p let p be Polynomial of n,L; ::_thesis: Support (Red (p,O)) c= Support p Support (Red (p,O)) = (Support p) \ {(HT (p,O))} by Lm17; hence Support (Red (p,O)) c= Support p by XBOOLE_1:36; ::_thesis: verum end; theorem :: TERMORD:36 for n being Ordinal for T being connected TermOrder of n for L being non trivial right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L holds Support (Red (p,T)) = (Support p) \ {(HT (p,T))} by Lm17; Lm18: for n being Ordinal for T being connected TermOrder of n for L being non trivial right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L holds (Red (p,T)) . (HT (p,T)) = 0. L proof let n be Ordinal; ::_thesis: for T being connected TermOrder of n for L being non trivial right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L holds (Red (p,T)) . (HT (p,T)) = 0. L let O be connected TermOrder of n; ::_thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L holds (Red (p,O)) . (HT (p,O)) = 0. L let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being Polynomial of n,L holds (Red (p,O)) . (HT (p,O)) = 0. L let p be Polynomial of n,L; ::_thesis: (Red (p,O)) . (HT (p,O)) = 0. L ( HT (p,O) in {(HT (p,O))} & Support (Red (p,O)) = (Support p) \ {(HT (p,O))} ) by Lm17, TARSKI:def_1; then not HT (p,O) in Support (Red (p,O)) by XBOOLE_0:def_5; hence (Red (p,O)) . (HT (p,O)) = 0. L by POLYNOM1:def_3; ::_thesis: verum end; Lm19: for n being Ordinal for O being connected TermOrder of n for L being non trivial right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L for b being bag of n st b <> HT (p,O) holds (Red (p,O)) . b = p . b proof let n be Ordinal; ::_thesis: for O being connected TermOrder of n for L being non trivial right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L for b being bag of n st b <> HT (p,O) holds (Red (p,O)) . b = p . b let O be connected TermOrder of n; ::_thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L for b being bag of n st b <> HT (p,O) holds (Red (p,O)) . b = p . b let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being Polynomial of n,L for b being bag of n st b <> HT (p,O) holds (Red (p,O)) . b = p . b let p be Polynomial of n,L; ::_thesis: for b being bag of n st b <> HT (p,O) holds (Red (p,O)) . b = p . b let b be bag of n; ::_thesis: ( b <> HT (p,O) implies (Red (p,O)) . b = p . b ) A1: b is Element of Bags n by PRE_POLY:def_12; assume b <> HT (p,O) ; ::_thesis: (Red (p,O)) . b = p . b then not b in {(HT (p,O))} by TARSKI:def_1; then A2: not b in Support (HM (p,O)) by Lm12; thus (Red (p,O)) . b = (p + (- (HM (p,O)))) . b by POLYNOM1:def_6 .= (p . b) + ((- (HM (p,O))) . b) by POLYNOM1:15 .= (p . b) + (- ((HM (p,O)) . b)) by POLYNOM1:17 .= (p . b) + (- (0. L)) by A2, A1, POLYNOM1:def_3 .= (p . b) + (0. L) by RLVECT_1:12 .= p . b by RLVECT_1:4 ; ::_thesis: verum end; theorem :: TERMORD:37 for n being Ordinal for T being connected TermOrder of n for L being non trivial right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L holds Support ((HM (p,T)) + (Red (p,T))) = Support p proof let n be Ordinal; ::_thesis: for T being connected TermOrder of n for L being non trivial right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L holds Support ((HM (p,T)) + (Red (p,T))) = Support p let O be connected TermOrder of n; ::_thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L holds Support ((HM (p,O)) + (Red (p,O))) = Support p let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being Polynomial of n,L holds Support ((HM (p,O)) + (Red (p,O))) = Support p let p be Polynomial of n,L; ::_thesis: Support ((HM (p,O)) + (Red (p,O))) = Support p A1: now__::_thesis:_for_u_being_set_st_u_in_Support_p_holds_ u_in_Support_((HM_(p,O))_+_(Red_(p,O))) let u be set ; ::_thesis: ( u in Support p implies u in Support ((HM (p,O)) + (Red (p,O))) ) assume A2: u in Support p ; ::_thesis: u in Support ((HM (p,O)) + (Red (p,O))) then reconsider u9 = u as Element of Bags n ; reconsider u9 = u9 as bag of n ; A3: p . u9 <> 0. L by A2, POLYNOM1:def_3; now__::_thesis:_(_(_u9_=_HT_(p,O)_&_u9_in_Support_((HM_(p,O))_+_(Red_(p,O)))_)_or_(_u9_<>_HT_(p,O)_&_u9_in_Support_((HM_(p,O))_+_(Red_(p,O)))_)_) percases ( u9 = HT (p,O) or u9 <> HT (p,O) ) ; caseA4: u9 = HT (p,O) ; ::_thesis: u9 in Support ((HM (p,O)) + (Red (p,O))) then A5: p . (HT (p,O)) <> 0. L by A2, POLYNOM1:def_3; ((HM (p,O)) + (Red (p,O))) . u9 = ((HM (p,O)) . u9) + ((Red (p,O)) . u9) by POLYNOM1:15 .= ((HM (p,O)) . u9) + (0. L) by A4, Lm18 .= (HM (p,O)) . u9 by RLVECT_1:4 .= HC (p,O) by A4, Lm8 ; hence u9 in Support ((HM (p,O)) + (Red (p,O))) by A5, POLYNOM1:def_3; ::_thesis: verum end; caseA6: u9 <> HT (p,O) ; ::_thesis: u9 in Support ((HM (p,O)) + (Red (p,O))) ((HM (p,O)) + (Red (p,O))) . u9 = ((HM (p,O)) . u9) + ((Red (p,O)) . u9) by POLYNOM1:15 .= ((HM (p,O)) . u9) + (p . u9) by A6, Lm19 .= (0. L) + (p . u9) by A6, Th19 .= p . u9 by RLVECT_1:4 ; hence u9 in Support ((HM (p,O)) + (Red (p,O))) by A3, POLYNOM1:def_3; ::_thesis: verum end; end; end; hence u in Support ((HM (p,O)) + (Red (p,O))) ; ::_thesis: verum end; now__::_thesis:_for_u_being_set_st_u_in_Support_((HM_(p,O))_+_(Red_(p,O)))_holds_ u_in_Support_p let u be set ; ::_thesis: ( u in Support ((HM (p,O)) + (Red (p,O))) implies u in Support p ) assume A7: u in Support ((HM (p,O)) + (Red (p,O))) ; ::_thesis: u in Support p then reconsider u9 = u as Element of Bags n ; reconsider u9 = u9 as bag of n ; A8: ((HM (p,O)) + (Red (p,O))) . u9 <> 0. L by A7, POLYNOM1:def_3; now__::_thesis:_(_(_u9_=_HT_(p,O)_&_u9_in_Support_p_)_or_(_u9_<>_HT_(p,O)_&_u9_in_Support_p_)_) percases ( u9 = HT (p,O) or u9 <> HT (p,O) ) ; caseA9: u9 = HT (p,O) ; ::_thesis: u9 in Support p ((HM (p,O)) + (Red (p,O))) . u9 = ((HM (p,O)) . u9) + ((Red (p,O)) . u9) by POLYNOM1:15 .= ((HM (p,O)) . (HT (p,O))) + (0. L) by A9, Lm18 .= (HM (p,O)) . (HT (p,O)) by RLVECT_1:4 .= p . u9 by A9, Lm8 ; hence u9 in Support p by A8, POLYNOM1:def_3; ::_thesis: verum end; caseA10: u9 <> HT (p,O) ; ::_thesis: u9 in Support p ((HM (p,O)) + (Red (p,O))) . u9 = ((HM (p,O)) . u9) + ((Red (p,O)) . u9) by POLYNOM1:15 .= (0. L) + ((Red (p,O)) . u9) by A10, Th19 .= (Red (p,O)) . u9 by RLVECT_1:4 .= p . u by A10, Lm19 ; hence u9 in Support p by A8, POLYNOM1:def_3; ::_thesis: verum end; end; end; hence u in Support p ; ::_thesis: verum end; hence Support ((HM (p,O)) + (Red (p,O))) = Support p by A1, TARSKI:1; ::_thesis: verum end; theorem :: TERMORD:38 for n being Ordinal for T being connected TermOrder of n for L being non trivial right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L holds (HM (p,T)) + (Red (p,T)) = p proof let n be Ordinal; ::_thesis: for T being connected TermOrder of n for L being non trivial right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L holds (HM (p,T)) + (Red (p,T)) = p let O be connected TermOrder of n; ::_thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L holds (HM (p,O)) + (Red (p,O)) = p let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being Polynomial of n,L holds (HM (p,O)) + (Red (p,O)) = p let p be Polynomial of n,L; ::_thesis: (HM (p,O)) + (Red (p,O)) = p A1: now__::_thesis:_for_x_being_set_st_x_in_Bags_n_holds_ p_._x_=_((HM_(p,O))_+_(Red_(p,O)))_._x let x be set ; ::_thesis: ( x in Bags n implies p . x = ((HM (p,O)) + (Red (p,O))) . x ) assume x in Bags n ; ::_thesis: p . x = ((HM (p,O)) + (Red (p,O))) . x then reconsider x9 = x as Element of Bags n ; now__::_thesis:_(_(_x_=_HT_(p,O)_&_((HM_(p,O))_+_(Red_(p,O)))_._x_=_p_._x_)_or_(_x_<>_HT_(p,O)_&_p_._x_=_((HM_(p,O))_+_(Red_(p,O)))_._x_)_) percases ( x = HT (p,O) or x <> HT (p,O) ) ; caseA2: x = HT (p,O) ; ::_thesis: ((HM (p,O)) + (Red (p,O))) . x = p . x hence ((HM (p,O)) + (Red (p,O))) . x = ((HM (p,O)) . (HT (p,O))) + ((Red (p,O)) . (HT (p,O))) by POLYNOM1:15 .= ((HM (p,O)) . (HT (p,O))) + (0. L) by Lm18 .= (HM (p,O)) . (HT (p,O)) by RLVECT_1:4 .= p . x by A2, Lm8 ; ::_thesis: verum end; caseA3: x <> HT (p,O) ; ::_thesis: p . x = ((HM (p,O)) + (Red (p,O))) . x ((HM (p,O)) + (Red (p,O))) . x9 = ((HM (p,O)) . x9) + ((Red (p,O)) . x9) by POLYNOM1:15 .= ((HM (p,O)) . x9) + (p . x9) by A3, Lm19 .= (0. L) + (p . x9) by A3, Th19 .= p . x9 by RLVECT_1:4 ; hence p . x = ((HM (p,O)) + (Red (p,O))) . x ; ::_thesis: verum end; end; end; hence p . x = ((HM (p,O)) + (Red (p,O))) . x ; ::_thesis: verum end; ( dom p = Bags n & dom ((HM (p,O)) + (Red (p,O))) = Bags n ) by FUNCT_2:def_1; hence (HM (p,O)) + (Red (p,O)) = p by A1, FUNCT_1:2; ::_thesis: verum end; theorem :: TERMORD:39 for n being Ordinal for T being connected TermOrder of n for L being non trivial right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L holds (Red (p,T)) . (HT (p,T)) = 0. L by Lm18; theorem :: TERMORD:40 for n being Ordinal for T being connected TermOrder of n for L being non trivial right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of n,L for b being bag of n st b in Support p & b <> HT (p,T) holds (Red (p,T)) . b = p . b by Lm19;