:: by Christoph Schwarzweller

::

:: Received December 20, 2002

:: Copyright (c) 2002-2019 Association of Mizar Users

registration

existence

ex b_{1} being non trivial addLoopStr st

( b_{1} is add-associative & b_{1} is right_complementable & b_{1} is right_zeroed )

end;
ex b

( b

proof end;

definition
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 );

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 )

for b1, b2 being bag of X holds

( b1 divides b2 iff ex b being bag of X st b2 = b1 + b )

proof 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)

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 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;

coherence

m1 *' m2 is monomial-like

end;
let L be non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ;

let m1, m2 be Monomial of n,L;

coherence

m1 *' m2 is monomial-like

proof 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;

coherence

c1 *' c2 is Constant

end;
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ;

let c1, c2 be ConstPoly of n,L;

coherence

c1 *' c2 is Constant

proof 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))

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 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))

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 end;

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 end;

registration

let n be Ordinal;

ex b_{1} being TermOrder of n st

( b_{1} is admissible & b_{1} is connected )

end;
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 b

( b

proof end;

:: theorem 5.5 (ii), p. 190

registration

let n be Nat;

for b_{1} being admissible TermOrder of n holds b_{1} is well_founded

end;
cluster total reflexive antisymmetric transitive admissible -> well_founded admissible for Element of K19(K20((Bags n),(Bags n)));

coherence for b

proof end;

:: deftheorem 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 );

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 );

:: deftheorem 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 ) );

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;

correctness

coherence

( ( b1 <= b2,T implies b1 is bag of n ) & ( not b1 <= b2,T implies b2 is bag of n ) );

consistency

for b_{1} being bag of n holds verum;

;

correctness

coherence

( ( b2 <= b1,T implies b1 is bag of n ) & ( not b2 <= b1,T implies b2 is bag of n ) );

consistency

for b_{1} being bag of n holds verum;

;

end;
let T be TermOrder of n;

let b1, b2 be bag of n;

correctness

coherence

( ( b1 <= b2,T implies b1 is bag of n ) & ( not b1 <= b2,T implies b2 is bag of n ) );

consistency

for b

;

correctness

coherence

( ( b2 <= b1,T implies b1 is bag of n ) & ( not b2 <= b1,T implies b2 is bag of n ) );

consistency

for b

;

:: 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 ) );

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 ) );

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 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 end;

Lm4: for n being Ordinal

for T being TermOrder of n

for b being bag of n holds b in field T

proof 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 )

for T being connected TermOrder of n

for b1, b2 being bag of n holds

( b1 <= b2,T iff not b2 < b1,T )

proof 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 end;

theorem :: TERMORD:6

theorem :: TERMORD:7

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

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 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 by BAGORDER:def 5;

for T being admissible TermOrder of n

for b being bag of n holds EmptyBag n <= b,T by BAGORDER:def 5;

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

for T being admissible TermOrder of n

for b1, b2 being bag of n st b1 divides b2 holds

b1 <= b2,T

proof 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 )

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 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 )

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 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 )

by Def4, Def5;

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 )

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 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 )

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 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) )

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 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 )

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 end;

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;

ex b_{1} being Element of Bags n st

( ( Support p = {} & b_{1} = EmptyBag n ) or ( b_{1} in Support p & ( for b being bag of n st b in Support p holds

b <= b_{1},T ) ) )

for b_{1}, b_{2} being Element of Bags n st ( ( Support p = {} & b_{1} = EmptyBag n ) or ( b_{1} in Support p & ( for b being bag of n st b in Support p holds

b <= b_{1},T ) ) ) & ( ( Support p = {} & b_{2} = EmptyBag n ) or ( b_{2} in Support p & ( for b being bag of n st b in Support p holds

b <= b_{2},T ) ) ) holds

b_{1} = b_{2}

end;
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 ( ( 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 ) ) );

ex b

( ( Support p = {} & b

b <= b

proof end;

uniqueness for b

b <= b

b <= b

b

proof 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 b_{5} being Element of Bags n holds

( b_{5} = HT (p,T) iff ( ( Support p = {} & b_{5} = EmptyBag n ) or ( b_{5} in Support p & ( for b being bag of n st b in Support p holds

b <= b_{5},T ) ) ) );

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 b

( b

b <= b

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;

correctness

coherence

p . (HT (p,T)) is Element of L;

;

end;
let T be connected TermOrder of n;

let L be non empty ZeroStr ;

let p be Polynomial of n,L;

correctness

coherence

p . (HT (p,T)) is Element of L;

;

:: 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));

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;

correctness

coherence

Monom ((HC (p,T)),(HT (p,T))) is Monomial of n,L;

;

end;
let T be connected TermOrder of n;

let L be non empty ZeroStr ;

let p be Polynomial of n,L;

correctness

coherence

Monom ((HC (p,T)),(HT (p,T))) is Monomial of n,L;

;

:: 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)));

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 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 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 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 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;

coherence

HM (p,T) is non-zero

not HC (p,T) is zero

end;
let T be connected TermOrder of n;

let L be non trivial ZeroStr ;

let p be non-zero Polynomial of n,L;

coherence

HM (p,T) is non-zero

proof end;

coherence not HC (p,T) is zero

proof 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 end;

theorem :: TERMORD:17

theorem :: TERMORD:18

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

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 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 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

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 end;

theorem :: TERMORD:21

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) )

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 end;

theorem :: TERMORD:23

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) )

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 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 )

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 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)

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 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)

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 end;

theorem :: TERMORD:28

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 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 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)

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 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 ) }

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 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))

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 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))

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 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))

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 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

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 end;

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;

coherence

p - (HM (p,T)) is Polynomial of n,L ;

end;
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;

coherence

p - (HM (p,T)) is Polynomial of n,L ;

:: 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));

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 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 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 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

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 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;

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 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 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

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 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

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 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;

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;

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;